---

Step * 1 of Lemma canonicalizable-product


1. [T] : Type
2. [B] : T ⟶ Type
3. ∀t:T. ∃x:Base. (t = x ∈ T)
4. ∀x:T. ∀t:B[x].  ∃x1:Base. (t = x1 ∈ B[x])
5. x : T
6. t1 : B[x]
⊢ ∃x@0:Base. (<x, t1> = x@0 ∈ (x:T × B[x]))
BY
{ (((D 3 With ⌜x⌝  THENA Auto) THEN (InstHyp [⌜x⌝;⌜t1⌝] 3⋅ THENA Auto)) THEN ExRepD THEN RenameVar `b' (-4)) }

1
1. [T] : Type
2. [B] : T ⟶ Type
3. ∀x:T. ∀t:B[x].  ∃x1:Base. (t = x1 ∈ B[x])
4. x : T
5. t1 : B[x]
6. b : Base
7. x = b ∈ T
8. x1 : Base
9. t1 = x1 ∈ B[x]
⊢ ∃x@0:Base. (<x, t1> = x@0 ∈ (x:T × B[x]))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [B]  :  T  {}\mrightarrow{}  Type
3.  \mforall{}t:T.  \mexists{}x:Base.  (t  =  x)
4.  \mforall{}x:T.  \mforall{}t:B[x].    \mexists{}x1:Base.  (t  =  x1)
5.  x  :  T
6.  t1  :  B[x]
\mvdash{}  \mexists{}x@0:Base.  (<x,  t1>  =  x@0)


By

---

Latex:
(((D  3  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}t1\mkleeneclose{}]  3\mcdot{}  THENA  Auto))
  THEN  ExRepD
  THEN  RenameVar  `b'  (-4))

---

Home Index