---

Step * of Lemma equipollent-product-assoc

∀[A,B,C:Type].  A × B × C ~ A × B × C
BY
{ ((Auto THEN With ⌜λx.let a,b,c = x in <<a, b>, c>⌝ (D 0)⋅) THEN Auto) }

1
1. [A] : Type
2. [B] : Type
3. [C] : Type
⊢ Bij(A × B × C;A × B × C;λx.let a,b,c = x in 
                             <<a, b>, c>)

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].    A  \mtimes{}  B  \mtimes{}  C  \msim{}  A  \mtimes{}  B  \mtimes{}  C


By

---

Latex:
((Auto  THEN  With  \mkleeneopen{}\mlambda{}x.let  a,b,c  =  x  in  <<a,  b>,  c>\mkleeneclose{}  (D  0)\mcdot{})  THEN  Auto)

---

Home Index