---

Step * of Lemma permutations-list_wf

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

---

Latex:

---

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


By

---

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

---

Home Index