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