-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.