# Some inference rules

For each of the following theorems,
- Verify that its statement is a proposition,
- Prove it (with/without
`Auto`)
- Print the proof term

Lemma all_perm :
forall (A:Type) (P:A -> A -> Prop),
(forall x y:A, P x y) ->
forall x y:A, P y x.
Lemma resolution :
forall (A:Type) (P Q R S:A -> Prop),
(forall a:A, Q a -> R a -> S a) ->
(forall b:A, P b -> Q b) ->
forall c:A, P c -> R c -> S c.

## Solution

This file

Going home

Pierre Castéran