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 include "Legacy-1/definitions.ma".
18 cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind
19 cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/sym_eq.con
20 cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/trans_eq.con
21 cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq_ind.con
22 cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/eq_ind_r.con
23 cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq_rec.con
24 cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/eq_rec_r.con
25 cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq_rect.con
26 cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/eq_rect_r.con
27 cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/f_equal.con
28 cic:/matita/LAMBDA-TYPES/Legacy-2/preamble/f_equal_sym.con.
31 cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/True.ind.
33 cic:/matita/LAMBDA-TYPES/Legacy-1/preamble/False.ind.
35 cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/absurd.con.
37 interpretation "Coq's natural plus" 'plus x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/plus.con x y).
38 interpretation "Coq's natural minus" 'minus x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/minus.con x y).
39 interpretation "Coq's logical and" 'and x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/land.ind#xpointer(1/1) x y).
40 interpretation "Coq's logical or" 'or x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/or.ind#xpointer(1/1) x y).
41 interpretation "Coq's logical not" 'not x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/not.con x).
42 interpretation "Coq's exists" 'exists \eta.x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/ex.ind#xpointer(1/1) _ x).
43 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).
44 interpretation "Coq's natural 'less than'" 'lt x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/lt.con x y).
45 interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind#xpointer(1/1) _ x y).
47 theorem f_equal_sym: \forall A,B:Set.\forall f:A\to B.\forall x,y.
48 x = y \to (f y) = (f x).
50 apply cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/f_equal.con.