---

Step * 1 of Lemma equipollent-product-assoc


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>)
BY
{ (RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto))
   THEN Try ((DVar `a1' THEN DVar `a4' THEN DVar `a2' THEN DVar `a8' THEN All Reduce THEN Auto))
   ) }

1
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))

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [C]  :  Type
\mvdash{}  Bij(A  \mtimes{}  B  \mtimes{}  C;A  \mtimes{}  B  \mtimes{}  C;\mlambda{}x.let  a,b,c  =  x  in 
                                                          <<a,  b>,  c>)


By

---

Latex:
(RepeatFor  2  ((D  0  THEN  Reduce  0  THEN  Auto))
  THEN  Try  ((DVar  `a1'  THEN  DVar  `a4'  THEN  DVar  `a2'  THEN  DVar  `a8'  THEN  All  Reduce  THEN  Auto))
  )

---

Home Index