(**************************************************************************)
set "baseuri" "cic:/matita/tests/inversion/".
-include "coq.ma".
+include "legacy/coq.ma".
inductive nat : Set \def
O : nat
leO : le n n
| leS : \forall m. le n m \to le n (S m).
+theorem le_inv:
+ \forall n,m.
+ \forall P: nat -> nat -> Prop.
+ ? -> ? -> le n m -> P n m.
+[7:
+ intros;
+ inversion H;
+ [ apply x
+ | simplify;
+ apply x1
+ ]
+| skip
+| skip
+| skip
+| skip
+| skip
+| skip
+]
+qed.
inductive ledx : nat \to nat \to Prop \def
ledxO : \forall n. ledx n n