X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprocedural%2Flibrary%2Fpreamble.ma;h=5bad8268511dea8b494f6a3dbb965b89ee019603;hb=4446f96e1829f1a82fc71cb49d8ddc392e73b155;hp=89ee1a360f99c4e726c0dc58f6b520362eca1619;hpb=3bfc56cd9b5afe52c3abfbef886ce82efa3bb3a3;p=helm.git

diff --git a/helm/software/matita/contribs/procedural/library/preamble.ma b/helm/software/matita/contribs/procedural/library/preamble.ma
index 89ee1a360..5bad82685 100644
--- a/helm/software/matita/contribs/procedural/library/preamble.ma
+++ b/helm/software/matita/contribs/procedural/library/preamble.ma
@@ -12,38 +12,21 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(*
+default "true" cic:/matita/logic/connectives/True.ind.
 
-default "equality"
- cic:/Coq/Init/Logic/eq.ind
- cic:/Coq/Init/Logic/sym_eq.con
- cic:/Coq/Init/Logic/trans_eq.con
- cic:/Coq/Init/Logic/eq_ind.con
- cic:/Coq/Init/Logic/eq_ind_r.con
- cic:/Coq/Init/Logic/eq_rec.con
- cic:/Coq/Init/Logic/eq_rec_r.con
- cic:/Coq/Init/Logic/eq_rect.con
- cic:/Coq/Init/Logic/eq_rect_r.con
- cic:/Coq/Init/Logic/f_equal.con
- cic:/matita/procedural/Coq/preamble/f_equal1.con.
-
-default "true"
- cic:/Coq/Init/Logic/True.ind. 
-default "false"
- cic:/Coq/Init/Logic/False.ind. 
-default "absurd"
- cic:/Coq/Init/Logic/absurd.con. 
-
-interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y).
+default "false" cic:/matita/logic/connectives/False.ind.
 
-theorem f_equal1 : \forall A,B:Type.\forall f:A\to B.\forall x,y:A.
-  x = y \to (f y) = (f x).
-  intros.
-  symmetry.
-  apply cic:/Coq/Init/Logic/f_equal.con.
-  assumption.
-qed.
+default "absurd" cic:/matita/logic/connectives/absurd.con.
 
-alias id "land" = "cic:/matita/procedural/Coq/Init/Logic/and.ind#xpointer(1/1)".
-
-*)
+default "equality"
+ cic:/matita/logic/equality/eq.ind
+ cic:/matita/logic/equality/sym_eq.con
+ cic:/matita/logic/equality/transitive_eq.con
+ cic:/matita/logic/equality/eq_ind.con
+ cic:/matita/logic/equality/eq_elim_r.con
+ cic:/matita/logic/equality/eq_rec.con
+ cic:/matita/logic/equality/eq_elim_r'.con
+ cic:/matita/logic/equality/eq_rect.con
+ cic:/matita/logic/equality/eq_elim_r''.con
+ cic:/matita/logic/equality/eq_f.con
+ cic:/matita/logic/equality/eq_OF_eq.con.