-lemma extract_pair : ∀A,B,C,D. ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
-((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
-∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
-#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
+\ 5img class="anchor" src="icons/tick.png" id="extract_pair"\ 6lemma extract_pair : ∀A,B,C,D. ∀u:A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B. ∀Q:A → B → C\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6D. ∀x,y.
+((let 〈a,b〉 ≝ u in Q a b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6x,y\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6) →
+\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6a,b\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6a,b\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 u \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 Q a b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6x,y\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6.
+#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 @E1 qed.