---

Step * of Lemma app_permf_wf

∀m,n:ℕ. ∀p:ℕm ⟶ ℕm. ∀q:ℕn ⟶ ℕn.  (app_permf(m;n;p;q) ∈ ℕm + n ⟶ ℕm + n)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}m,n:\mBbbN{}.  \mforall{}p:\mBbbN{}m  {}\mrightarrow{}  \mBbbN{}m.  \mforall{}q:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n.    (app\_permf(m;n;p;q)  \mmember{}  \mBbbN{}m  +  n  {}\mrightarrow{}  \mBbbN{}m  +  n)


By

---

Latex:
ProveWfLemma

---

Home Index