From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Tue, 11 Oct 2011 11:09:25 +0000 (+0000)
Subject: commit by user utente1
X-Git-Tag: make_still_working~2219
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8baa4aabe6cc848c6a3ecd7a08e1bab9edc8bee1;p=helm.git

commit by user utente1
---

diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma
index f14392e93..ef8da2f19 100644
--- a/weblib/arithmetics/nat.ma
+++ b/weblib/arithmetics/nat.ma
@@ -389,7 +389,7 @@ apply (not_le_Sn_n ? H3).
 qed. *)
 
 theorem not_eq_to_le_to_lt: ∀n,m. na title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/am → na title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am → na title="natural 'less than'" href="cic:/fakeuri.def(1)"</am.
-#n #m #Hneq #Hle cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a ?? Hle) //
+#n #m #Hneq #Hle cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(6)"le_to_or_lt_eq/a ?? Hle) //
 #Heq /3/ qed.
 (*
 nelim (Hneq Heq) qed. *)
@@ -478,7 +478,7 @@ theorem increasing_to_le2: ∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0
   ∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. f a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a title="exists" href="cic:/fakeuri.def(1)"∃/ai. f i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m a title="logical and" href="cic:/fakeuri.def(1)"∧/a m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i).
 #f #incr #m #lem (elim lem)
   [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ? ? a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a) /2/
-  |#n #len * #a * #len #ltnr (cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … ltnr)) #H
+  |#n #len * #a * #len #ltnr (cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(6)"le_to_or_lt_eq/a … ltnr)) #H
     [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ? ? a) % /2/ 
     |@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ? ? (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a a)) % //
     ]
@@ -488,7 +488,7 @@ qed.
 theorem increasing_to_injective: ∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
   a href="cic:/matita/arithmetics/nat/increasing.def(2)"increasing/a f → a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a f.
 #f #incr #n #m cases(a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a n m)
-  [#lenm cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … lenm) //
+  [#lenm cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(6)"le_to_or_lt_eq/a … lenm) //
    #lenm #eqf @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … eqf) @a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"lt_to_not_eq/a 
    @a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"increasing_to_monotonic/a //
   |#nlenm #eqf @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … eqf) @a href="cic:/matita/basics/logic/sym_not_eq.def(4)"sym_not_eq/a 
@@ -700,14 +700,14 @@ qed.
 theorem lt_to_le_to_lt_times: 
 ∀n,m,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → p a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a q → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q → na title="natural times" href="cic:/fakeuri.def(1)"*/ap a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a ma title="natural times" href="cic:/fakeuri.def(1)"*/aq.
 #n #m #p #q #ltnm #lepq #posq
-@(a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a ? (na title="natural times" href="cic:/fakeuri.def(1)"*/aq))
+@(a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(5)"le_to_lt_to_lt/a ? (na title="natural times" href="cic:/fakeuri.def(1)"*/aq))
   [@a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a //
-  |@a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(9)"monotonic_lt_times_l/a //
+  |@a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(10)"monotonic_lt_times_l/a //
   ]
 qed.
 
 theorem lt_times:∀n,m,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural 'less than'" href="cic:/fakeuri.def(1)"</am → pa title="natural 'less than'" href="cic:/fakeuri.def(1)"</aq → na title="natural times" href="cic:/fakeuri.def(1)"*/ap a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a ma title="natural times" href="cic:/fakeuri.def(1)"*/aq.
-#n #m #p #q #ltnm #ltpq @a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(10)"lt_to_le_to_lt_times/a/2/
+#n #m #p #q #ltnm #ltpq @a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"lt_to_le_to_lt_times/aspan style="text-decoration: underline;" /span/2/
 qed.
 
 theorem lt_times_n_to_lt_l: 
@@ -811,7 +811,8 @@ napplyS (not_eq_to_le_to_lt n (S m) H H1)
 qed. *)
 
 theorem eq_minus_S_pred: ∀n,m. n a title="natural minus" href="cic:/fakeuri.def(1)"-/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a(n a title="natural minus" href="cic:/fakeuri.def(1)"-/am).
-@a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a normalize // qed.
+@a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a normalize //
+qed.
 
 theorem plus_minus:
 ∀m,n,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → (na title="natural minus" href="cic:/fakeuri.def(1)"-/am)a title="natural plus" href="cic:/fakeuri.def(1)"+/ap a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (na title="natural plus" href="cic:/fakeuri.def(1)"+/ap)a title="natural minus" href="cic:/fakeuri.def(1)"-/am.
@@ -844,7 +845,7 @@ qed.
 
 theorem minus_pred_pred : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → 
 a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a n a title="natural minus" href="cic:/fakeuri.def(1)"-/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural minus" href="cic:/fakeuri.def(1)"-/a m.
-#n #m #posn #posm @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"lt_O_n_elim/a n posn) @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"lt_O_n_elim/a m posm) //.
+#n #m #posn #posm @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(7)"lt_O_n_elim/a n posn) @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(7)"lt_O_n_elim/a m posm) //.
 qed.
 
 
@@ -910,7 +911,7 @@ qed.
 
 theorem le_minus_to_plus: ∀n,m,p. na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → na title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am.
 #n #m #p #lep @a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a
-  [|@a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(6)"le_plus_minus_m_m/a | @a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a // ]
+  [|@a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(8)"le_plus_minus_m_m/a | @a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a // ]
 qed.
 
 theorem le_minus_to_plus_r: ∀a,b,c. c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b → a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a c → a a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b.
@@ -930,22 +931,22 @@ theorem lt_minus_to_plus: ∀a,b,c. a a title="natural minus" href="cic:/fakeur
 qed.
 
 theorem lt_minus_to_plus_r: ∀a,b,c. a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a c → a a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b.
-#a #b #c #H @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(7)"le_plus_to_minus/a …))
+#a #b #c #H @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(9)"le_plus_to_minus/a …))
 @a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a //
 qed.
 
 theorem lt_plus_to_minus: ∀n,m,p. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am → na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p.
-#n #m #p #lenm #H normalize <a href="cic:/matita/arithmetics/nat/minus_Sn_m.def(5)"minus_Sn_m/a // @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(7)"le_plus_to_minus/a //
+#n #m #p #lenm #H normalize <a href="cic:/matita/arithmetics/nat/minus_Sn_m.def(5)"minus_Sn_m/a // @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(9)"le_plus_to_minus/a //
 qed.
 
 theorem lt_plus_to_minus_r: ∀a,b,c. a a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c a title="natural minus" href="cic:/fakeuri.def(1)"-/a b.
-#a #b #c #H @a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(7)"le_plus_to_minus_r/a //
+#a #b #c #H @a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(9)"le_plus_to_minus_r/a //
 qed. 
 
 theorem monotonic_le_minus_r: 
 ∀p,q,n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. q a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → na title="natural minus" href="cic:/fakeuri.def(1)"-/ap a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a na title="natural minus" href="cic:/fakeuri.def(1)"-/aq.
-#p #q #n #lepq @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(7)"le_plus_to_minus/a
-@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(6)"le_plus_minus_m_m/a ? q)) /2/
+#p #q #n #lepq @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(9)"le_plus_to_minus/a
+@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(8)"le_plus_minus_m_m/a ? q)) /2/
 qed.
 
 theorem eq_minus_O: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
@@ -956,7 +957,7 @@ qed.
 theorem distributive_times_minus: a href="cic:/matita/basics/relations/distributive.def(1)"distributive/a ? a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a a href="cic:/matita/arithmetics/nat/minus.fix(0,0,1)"minus/a.
 #a #b #c
 (cases (a href="cic:/matita/arithmetics/nat/decidable_lt.def(7)"decidable_lt/a b c)) #Hbc
- [> a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a /2/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a // 
+ [> a href="cic:/matita/arithmetics/nat/eq_minus_O.def(11)"eq_minus_O/a /2/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(11)"eq_minus_O/a // 
   @a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a /2/
  |@a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a (applyS a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a) <a href="cic:/matita/arithmetics/nat/distributive_times_plus.def(7)"distributive_times_plus/a 
   @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a (applyS a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a) /2/
@@ -968,7 +969,7 @@ cases (a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a
   [@a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a @a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a <a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a
    @a href="cic:/matita/arithmetics/nat/minus_to_plus.def(8)"minus_to_plus/a //
   |cut (n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a ma title="natural plus" href="cic:/fakeuri.def(1)"+/ap) [@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_n_Sn.def(1)"le_n_Sn/a …)) @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a //]
-   #H >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a /2/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a // 
+   #H >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(11)"eq_minus_O/a /2/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(11)"eq_minus_O/a // 
   ]
 qed.
 
@@ -1115,4 +1116,4 @@ lemma le_maxr: ∀i,n,m. a href="cic:/matita/arithmetics/nat/max.def(2)"max/a
 
 lemma to_max: ∀i,n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i.
 #i #n #m #leni #lemi normalize (cases (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m)) 
-normalize // qed.
+normalize // qed.
\ No newline at end of file
diff --git a/weblib/basics/relations.ma b/weblib/basics/relations.ma
index b31db23d7..3081fa96b 100644
--- a/weblib/basics/relations.ma
+++ b/weblib/basics/relations.ma
@@ -15,27 +15,27 @@ include "basics/logic.ma".
 definition relation : Type[0] → Type[0]
 ≝ λA.A→A→Prop. 
 
-definition reflexive: ∀A.∀R :relation A.Prop
+definition reflexive: ∀A.∀R :a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop
 ≝ λA.λR.∀x:A.R x x.
 
-definition symmetric: ∀A.∀R: relation A.Prop
+definition symmetric: ∀A.∀R: a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop
 ≝ λA.λR.∀x,y:A.R x y → R y x.
 
-definition transitive: ∀A.∀R:relation A.Prop
+definition transitive: ∀A.∀R:a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop
 ≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z.
 
-definition irreflexive: ∀A.∀R:relation A.Prop
-≝ λA.λR.∀x:A.¬(R x x).
+definition irreflexive: ∀A.∀R:a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop
+≝ λA.λR.∀x:A.a title="logical not" href="cic:/fakeuri.def(1)"¬/a(R x x).
 
-definition cotransitive: ∀A.∀R:relation A.Prop
-≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
+definition cotransitive: ∀A.∀R:a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop
+≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z a title="logical or" href="cic:/fakeuri.def(1)"∨/a R z y.
 
-definition tight_apart: ∀A.∀eq,ap:relation A.Prop
-≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧
-(eq x y → ¬(ap x y)).
+definition tight_apart: ∀A.∀eq,ap:a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop
+≝ λA.λeq,ap.∀x,y:A. (a title="logical not" href="cic:/fakeuri.def(1)"¬/a(ap x y) → eq x y) a title="logical and" href="cic:/fakeuri.def(1)"∧/a
+(eq x y → a title="logical not" href="cic:/fakeuri.def(1)"¬/a(ap x y)).
 
-definition antisymmetric: ∀A.∀R:relation A.Prop
-≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
+definition antisymmetric: ∀A.∀R:a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop
+≝ λA.λR.∀x,y:A. R x y → a title="logical not" href="cic:/fakeuri.def(1)"¬/a(R y x).
 
 (********** functions **********)
 
@@ -45,19 +45,19 @@ definition compose ≝
 interpretation "function composition" 'compose f g = (compose ? ? ? f g).
 
 definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
-≝ λA,B.λf.∀x,y:A.f x = f y → x=y.
+≝ λA,B.λf.∀x,y:A.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f y → xa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ay.
 
 definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
-≝λA,B.λf.∀z:B.∃x:A.z = f x.
+≝λA,B.λf.∀z:B.a title="exists" href="cic:/fakeuri.def(1)"∃/ax:A.z a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f x.
 
 definition commutative: ∀A:Type[0].∀f:A→A→A.Prop 
-≝ λA.λf.∀x,y.f x y = f y x.
+≝ λA.λf.∀x,y.f x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f y x.
 
 definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop
-≝ λA,B.λf.∀x,y.f x y = f y x.
+≝ λA,B.λf.∀x,y.f x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f y x.
 
 definition associative: ∀A:Type[0].∀f:A→A→A.Prop
-≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
+≝ λA.λf.∀x,y,z.f (f x y) z a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f x (f y z).
 
 (* functions and relations *)
 definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
@@ -66,25 +66,25 @@ definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
 
 (* functions and functions *)
 definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
-≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z).
+≝ λA.λf,g.∀x,y,z:A. f x (g y z) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g (f x y) (f x z).
 
 definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop
-≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) = g (f x y) (f x z).
+≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g (f x y) (f x z).
 
 lemma injective_compose : ∀A,B,C,f,g.
-injective A B f → injective B C g → injective A C (λx.g (f x)).
+a href="cic:/matita/basics/relations/injective.def(1)"injective/a A B f → a href="cic:/matita/basics/relations/injective.def(1)"injective/a B C g → a href="cic:/matita/basics/relations/injective.def(1)"injective/a A C (λx.g (f x)).
 /3/; qed.
 
 (* extensional equality *)
 
 definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
-λA.λP,Q.∀a.iff (P a) (Q a).
+λA.λP,Q.∀a.a href="cic:/matita/basics/logic/iff.def(1)"iff/a (P a) (Q a).
 
 definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
-λA,B.λR,S.∀a.∀b.iff (R a b) (S a b).
+λA,B.λR,S.∀a.∀b.a href="cic:/matita/basics/logic/iff.def(1)"iff/a (R a b) (S a b).
 
 definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
-λA,B.λf,g.∀a.f a = g a.
+λA,B.λf,g.∀a.f a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g a.
 
 notation " x \eqP y " non associative with precedence 45 
 for @{'eqP A $x $y}.
@@ -102,5 +102,4 @@ notation " f \eqF g " non associative with precedence 45
 for @{'eqF ? ? f g}.
 
 interpretation "functional extentional equality" 
-'eqF A B f g = (exteqF A B f g).
-
+'eqF A B f g = (exteqF A B f g).
\ No newline at end of file