X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Fjmeq.ma;h=7838f0e9778543a98145b2e3a99690d4e80fbce8;hb=f38fd769279794d0ca73c8945eac30e8b42e59be;hp=ad3aa937101c238a90ab7ac0ad921e357d1776b0;hpb=8f08fac33a366b2267b35af1a50ad3a9df8dbb88;p=helm.git

diff --git a/weblib/basics/jmeq.ma b/weblib/basics/jmeq.ma
index ad3aa9371..7838f0e97 100644
--- a/weblib/basics/jmeq.ma
+++ b/weblib/basics/jmeq.ma
@@ -11,82 +11,82 @@
 
 include "basics/logic.ma".
 
-inductive Sigma: Type[1] ≝
+img class="anchor" src="icons/tick.png" id="Sigma"inductive Sigma: Type[1] ≝
  mk_Sigma: ∀p1: Type[0]. p1 → Sigma.
 
-definition p1: Sigma → Type[0].
+img class="anchor" src="icons/tick.png" id="p1"definition p1: a href="cic:/matita/basics/jmeq/Sigma.ind(1,0,0)"Sigma/a → Type[0].
  #S cases S #Y #_ @Y
 qed.
 
-definition p2: ∀S:Sigma. p1 S.
+img class="anchor" src="icons/tick.png" id="p2"definition p2: ∀S:a href="cic:/matita/basics/jmeq/Sigma.ind(1,0,0)"Sigma/a. a href="cic:/matita/basics/jmeq/p1.def(1)"p1/a S.
  #S cases S #Y #x @x
 qed.
 
-inductive jmeq (A:Type[0]) (x:A) : ∀B:Type[0]. B →Prop ≝
+img class="anchor" src="icons/tick.png" id="jmeq"inductive jmeq (A:Type[0]) (x:A) : ∀B:Type[0]. B →Prop ≝
 jmrefl : jmeq A x A x.
 
-definition eqProp ≝ λA:Prop.eq A.
+img class="anchor" src="icons/tick.png" id="eqProp"definition eqProp ≝ λA:Prop.a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a A.
 
-lemma K : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
-#A #x #h @(refl ? h: eqProp ? ? ?).
+img class="anchor" src="icons/tick.png" id="K"lemma K : ∀A.∀x:A.∀h:xa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax. a href="cic:/matita/basics/jmeq/eqProp.def(1)" title="null"eqProp/a ? h (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A x).
+#A #x #h @(a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? h: a href="cic:/matita/basics/jmeq/eqProp.def(1)"eqProp/a ? ? ?).
 qed.
 
-definition cast:
- ∀A,B:Type[0].∀E:A=B. A → B.
+img class="anchor" src="icons/tick.png" id="cast"definition cast:
+ ∀A,B:Type[0].∀E:Aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aB. A → B.
  #A #B #E cases E #X @X
 qed.
 
-lemma tech1:
- ∀Aa,Bb:Sigma.∀E:Aa=Bb.
-  cast (p1 Aa) (p1 Bb) ? (p2 Aa) = p2 Bb.
+img class="anchor" src="icons/tick.png" id="tech1"lemma tech1:
+ ∀Aa,Bb:a href="cic:/matita/basics/jmeq/Sigma.ind(1,0,0)"Sigma/a.∀E:Aaa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aBb.
+  a href="cic:/matita/basics/jmeq/cast.def(1)"cast/a (a href="cic:/matita/basics/jmeq/p1.def(1)"p1/a Aa) (a href="cic:/matita/basics/jmeq/p1.def(1)"p1/a Bb) ? (a href="cic:/matita/basics/jmeq/p2.def(2)"p2/a Aa) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/jmeq/p2.def(2)"p2/a Bb.
  [2: >E %
  | #Aa #Bb #E >E cases Bb #B #b normalize % ]
 qed.
  
-lemma gral: ∀A.∀x,y:A.
- mk_Sigma A x = mk_Sigma A y → x=y.
- #A #x #y #E lapply (tech1 ?? E)
- generalize in ⊢ (??(???%?)? → ?) #E1
- normalize in E1; >(K ?? E1) normalize
+img class="anchor" src="icons/tick.png" id="gral"lemma gral: ∀A.∀x,y:A.
+ a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"mk_Sigma/a A x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"mk_Sigma/a A y → xa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ay.
+ #A #x #y #E lapply (a href="cic:/matita/basics/jmeq/tech1.def(3)"tech1/a ?? E)
+ generalize in ⊢ (??(???%?)? → ?); #E1
+ normalize in E1; >(a href="cic:/matita/basics/jmeq/K.def(2)"K/a ?? E1) normalize
  #H @H
 qed.
 
-axiom daemon: False.
+img class="anchor" src="icons/tick.png" id="daemon"axiom daemon: a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a.
 
-lemma jm_to_eq_sigma:
- ∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y.
+img class="anchor" src="icons/tick.png" id="jm_to_eq_sigma"lemma jm_to_eq_sigma:
+ ∀A,x,y. a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"jmeq/a A x A y → a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"mk_Sigma/a A x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"mk_Sigma/a A y.
  #A #x #y #E cases E in ⊢ (???%); %
 qed.
 
-definition curry:
+img class="anchor" src="icons/tick.png" id="curry"definition curry:
  ∀A,x.
-  (∀y. jmeq A x A y → Type[0]) →
-   (∀y. mk_Sigma A x = mk_Sigma A y → Type[0]).
- #A #x #f #y #E @(f y) >(gral ??? E) %
+  (∀y. a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"jmeq/a A x A y → Type[0]) →
+   (∀y. a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"mk_Sigma/a A x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"mk_Sigma/a A y → Type[0]).
+ #A #x #f #y #E @(f y) >(a href="cic:/matita/basics/jmeq/gral.def(4)"gral/a ??? E) %
 qed.
 
-lemma G : ∀A.∀x:A.∀P:∀y:A.mk_Sigma A x = mk_Sigma A y →Type[0].
- P x (refl ? (mk_Sigma A x)) → ∀y.∀h:mk_Sigma A x = mk_Sigma A y.
+img class="anchor" src="icons/tick.png" id="G"lemma G : ∀A.∀x:A.∀P:∀y:A.a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"mk_Sigma/a A x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"mk_Sigma/a A y →Type[0].
+ P x (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? (a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"mk_Sigma/a A x)) → ∀y.∀h:a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"mk_Sigma/a A x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"mk_Sigma/a A y.
   P y h.
- #A #x #P #H #y #E lapply (gral ??? E) #G generalize in match E;
+ #A #x #P #H #y #E lapply (a href="cic:/matita/basics/jmeq/gral.def(4)"gral/a ??? E) #G generalize in match E;
  @(match G
-    return λy.λ_. ∀e:mk_Sigma A x = mk_Sigma A y. P y e
+    return λy.λ_. ∀e:a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"mk_Sigma/a A x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"mk_Sigma/a A y. P y e
    with
     [refl ⇒ ?])
- #E <(sym_eq ??? (K ?? E)) @H
+ #E <(a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a ??? (a href="cic:/matita/basics/jmeq/K.def(2)"K/a ?? E)) @H
 qed.
 
-definition PP: ∀A:Prop.∀P:A → Type[0]. A → Type[0].
+img class="anchor" src="icons/tick.png" id="PP"definition PP: ∀A:Prop.∀P:A → Type[0]. A → Type[0].
  #A #P #a @(P a)
 qed.
 
-lemma E : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
- PP ? (P x) (jmrefl A x) → ∀y.∀h:jmeq A x A y.PP ? (P y) h.
- #A #a #P #H #b #E letin F ≝ (jm_to_eq_sigma ??? E)
- lapply (G ?? (curry ?? P) ?? F)
+img class="anchor" src="icons/tick.png" id="E"lemma E : ∀A.∀x:A.∀P:∀y:A.a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"jmeq/a A x A y→Type[0].
+ a href="cic:/matita/basics/jmeq/PP.def(1)"PP/a ? (P x) (a href="cic:/matita/basics/jmeq/jmeq.con(0,1,2)"jmrefl/a A x) → ∀y.∀h:a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"jmeq/a A x A y.a href="cic:/matita/basics/jmeq/PP.def(1)"PP/a ? (P y) h.
+ #A #a #P #H #b #E letin F ≝ (a href="cic:/matita/basics/jmeq/jm_to_eq_sigma.def(1)"jm_to_eq_sigma/a ??? E)
+ lapply (a href="cic:/matita/basics/jmeq/G.def(5)"G/a ?? (a href="cic:/matita/basics/jmeq/curry.def(5)"curry/a ?? P) ?? F)
   [ normalize //
-  | #H whd in H; @(H : PP ? (P b) ?) ]
+  | #H whd in H; @(H : a href="cic:/matita/basics/jmeq/PP.def(1)"PP/a ? (P b) ?) ]
 qed.
 
-lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
- P x (jmrefl A x) → ∀y.∀h:jmeq A x A y.P y h ≝ E.
+img class="anchor" src="icons/tick.png" id="jmeq_elim"lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"jmeq/a A x A y→Type[0].
+ P x (a href="cic:/matita/basics/jmeq/jmeq.con(0,1,2)"jmrefl/a A x) → ∀y.∀h:a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"jmeq/a A x A y.P y h ≝ a href="cic:/matita/basics/jmeq/E.def(6)"E/a.
\ No newline at end of file