1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/tests/inversion/".
18 inductive nat : Set \def
23 inductive le (n:nat) : nat \to Prop \def
25 | leS : \forall m. le n m \to le n (S m).
28 inductive ledx : nat \to nat \to Prop \def
29 ledxO : \forall n. ledx n n
30 | ledxS : \forall m.\forall n. ledx n m \to ledx n (S m).
33 alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
35 theorem test_inversion: \forall n. le n O \to n=O.
38 (* cut n=n \to O=O \to n=O.
39 apply Hcut; reflexivity. *)
40 (* elim H. BUG DI UNSHARING *)
41 (*apply (ledx_ind (\lambda x.\lambda y. n=x \to O=y \to x=y) ? ? ? ? H).*)
42 simplify. intros. reflexivity.
43 simplify. intros. discriminate H3.