(**************************************************************************)
set "baseuri" "cic:/matita/tests/inversion2/".
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
inductive nat : Set \def
O : nat
(* 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.