---

Step * of Lemma ext2Cantor_eq

∀[s:𝔹 List]. ∀[d:𝔹].  (ext2Cantor(||s||;λx.s[x];d) = extl2Cantor(s;d) ∈ (ℕ ⟶ 𝔹))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``ext2Cantor extl2Cantor`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[s:\mBbbB{}  List].  \mforall{}[d:\mBbbB{}].    (ext2Cantor(||s||;\mlambda{}x.s[x];d)  =  extl2Cantor(s;d))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``ext2Cantor  extl2Cantor``  0  THEN  Auto)

---

Home Index