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/LAMBDA-TYPES/Level-1/Preamble".
17 include "legacy/coq.ma".
19 (* FG/CSC: These aliases should disappear: we would like to write something
20 * like: "disambiguate in cic:/Coq/*"
22 alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
23 alias id "or" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)".
24 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
25 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
26 alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
27 alias id "le_trans" = "cic:/Coq/Arith/Le/le_trans.con".
28 alias id "le_plus_r" = "cic:/Coq/Arith/Plus/le_plus_r.con".
29 alias id "le" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)".
30 alias id "ex" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)".
31 alias id "ex2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1)".
32 alias id "true" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/1)".
33 alias id "false" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/2)".
34 alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".
35 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
36 alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
37 alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con".
38 alias id "or_introl" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/1)".
39 alias id "or_intror" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/2)".
40 alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con".
41 alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
42 alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)".
43 alias id "minus" = "cic:/Coq/Init/Peano/minus.con".
45 theorem f_equal: \forall A,B:Type. \forall f:A \to B.
46 \forall x,y:A. x = y \to f x = f y.
47 intros. elim H. reflexivity.
50 theorem sym_eq: \forall A:Type. \forall x,y:A. x = y \to y = x.
51 intros. rewrite > H. reflexivity.
54 theorem sym_not_eq: \forall A:Type. \forall x,y:A. x \neq y \to y \neq x.
55 unfold not. intros. apply H. symmetry. assumption.