---

Step * 1 1 of Lemma equipollent-product-assoc


1. [A] : Type
2. [B] : Type
3. [C] : Type
4. b : A × B × C@i
⊢ ∃a:A × B × C. (let a,b,c = a in <<a, b>, c> = b ∈ (A × B × C))
BY
{ ((D -1 THEN D -2) THEN InstConcl [⌜<b3, b4, b2>⌝]⋅ THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [C]  :  Type
4.  b  :  A  \mtimes{}  B  \mtimes{}  C@i
\mvdash{}  \mexists{}a:A  \mtimes{}  B  \mtimes{}  C.  (let  a,b,c  =  a  in  <<a,  b>,  c>  =  b)


By

---

Latex:
((D  -1  THEN  D  -2)  THEN  InstConcl  [\mkleeneopen{}<b3,  b4,  b2>\mkleeneclose{}]\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index