---

Step * 1 1 of Lemma canonicalizable-product


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]))
BY
{ (D 0 With ⌜<b, x1>⌝  THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(D  0  With  \mkleeneopen{}<b,  x1>\mkleeneclose{}    THEN  Auto)

---

Home Index