---

Step * of Lemma canonicalizable-product

∀[T:Type]. ∀[B:T ⟶ Type].  (canonicalizable(T) ⇒ (∀x:T. canonicalizable(B[x])) ⇒ canonicalizable(x:T × B[x]))
BY
{ (RepeatFor 2 (Intro) THEN RWO "canonicalizable-iff" 0 THEN Auto THEN D -1) }

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[B:T  {}\mrightarrow{}  Type].
    (canonicalizable(T)  {}\mRightarrow{}  (\mforall{}x:T.  canonicalizable(B[x]))  {}\mRightarrow{}  canonicalizable(x:T  \mtimes{}  B[x]))


By

---

Latex:
(RepeatFor  2  (Intro)  THEN  RWO  "canonicalizable-iff"  0  THEN  Auto  THEN  D  -1)

---

Home Index