---

Step * of Lemma functions-list_wf

∀[n,b:ℕ].  (functions-list(n;b) ∈ {P:(ℕn ⟶ ℕb) List| no_repeats(ℕn ⟶ ℕb;P) ∧ (∀f:ℕn ⟶ ℕb. (f ∈ P))} )
BY
{ (Fold `sq_exists` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[n,b:\mBbbN{}].
    (functions-list(n;b)  \mmember{}  \{P:(\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}b)  List|  no\_repeats(\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}b;P)  \mwedge{}  (\mforall{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}b.  (f  \mmember{}  P))\}  )


By

---

Latex:
(Fold  `sq\_exists`  0  THEN  ProveWfLemma)

---

Home Index