---

Step * of Lemma k-ext-iff

∀[k:ℕ]. ∀[A,B:ℕk ⟶ Type].  uiff(A ≡ B;∀i:ℕk. A i ≡ B i)
BY
{ (Unfold `k-ext` 0 THEN Auto THEN D 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[A,B:\mBbbN{}k  {}\mrightarrow{}  Type].    uiff(A  \mequiv{}  B;\mforall{}i:\mBbbN{}k.  A  i  \mequiv{}  B  i)


By

---

Latex:
(Unfold  `k-ext`  0  THEN  Auto  THEN  D  0  THEN  Auto)

---

Home Index