---

Step * 1 of Lemma fun2listCantor


1. f : ℕ0 ⟶ 𝔹
⊢ ∃l:𝔹 List. ((||l|| = 0 ∈ ℤ) ∧ (f = (λx.l[x]) ∈ (ℕ0 ⟶ 𝔹)))
BY
{ TACTIC:(InstConcl [⌜[]⌝]⋅ THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}0  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  \mexists{}l:\mBbbB{}  List.  ((||l||  =  0)  \mwedge{}  (f  =  (\mlambda{}x.l[x])))


By

---

Latex:
TACTIC:(InstConcl  [\mkleeneopen{}[]\mkleeneclose{}]\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index