(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/inversion/".
-include "legacy/coq.ma".
+set "baseuri" "cic:/matita/tests/inversion2/".
+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:
+theorem le_inv2:
\forall n,m.
\forall P: nat -> nat -> Prop.
? -> ? -> le n m -> P n m.
(* elim H. BUG DI UNSHARING *)
(*apply (ledx_ind (\lambda x.\lambda y. n=x \to O=y \to x=y) ? ? ? ? H).*)
simplify. intros. reflexivity.
- simplify. intros. discriminate H3.
+ simplify. intros. destruct H3.
qed.