X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLegacy-2%2Fpreamble.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLegacy-2%2Fpreamble.ma;h=a2c8a84ed1358d82d02d60b2a1c5694c54af07d1;hb=6ba374cbb94797e58cd997c5b41099dd9f679a57;hp=269e41d6aef9e114e92fd806edcc2ccf105df68f;hpb=78b677a78cbe8f6f71ebdcdff970d0cde8a8c1b8;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
index 269e41d6a..a2c8a84ed 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
@@ -13,28 +13,40 @@
 (**************************************************************************)
 
 include "Legacy-1/definitions.ma".
-(*
+
 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/legacy/coq/f_equal1.con.
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/sym_eq.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/trans_eq.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq_ind.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/eq_ind_r.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq_rec.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/eq_rec_r.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq_rect.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/eq_rect_r.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/f_equal.con
+ cic:/matita/LAMBDA-TYPES/Legacy-2/preamble/f_equal_sym.con.
 
 default "true"
- cic:/Coq/Init/Logic/True.ind. 
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/True.ind. 
 default "false"
- cic:/Coq/Init/Logic/False.ind. 
+ cic:/matita/LAMBDA-TYPES/Legacy-1/preamble/False.ind. 
 default "absurd"
- cic:/Coq/Init/Logic/absurd.con. 
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/absurd.con. 
 
-(* aritmetic operators *)
+interpretation "Coq's natural plus" 'plus x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/plus.con x y).
+interpretation "Coq's natural minus" 'minus x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/minus.con x y).
+interpretation "Coq's logical and" 'and x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/land.ind#xpointer(1/1) x y).
+interpretation "Coq's logical or" 'or x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/or.ind#xpointer(1/1) x y).
+interpretation "Coq's logical not" 'not x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/not.con x).
+interpretation "Coq's exists" 'exists \eta.x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/ex.ind#xpointer(1/1) _ x).
+interpretation "Coq's natural 'less or equal to'" 'leq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/le.ind#xpointer(1/1) x y).
+interpretation "Coq's natural 'less than'" 'lt x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/lt.con x y).
+interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind#xpointer(1/1) _ x y).
 
-interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
-*)
+theorem f_equal_sym: \forall A,B:Set.\forall f:A\to B.\forall x,y.
+                     x = y \to (f y) = (f x).
+  intros; symmetry.
+  apply cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/f_equal.con.
+  assumption.
+qed.