---

Step * of Lemma make-strict_wf

∀[alpha:ℕ ⟶ ℕ]. (make-strict(alpha) ∈ StrictInc)
BY
{ (Auto THEN (Assert make-strict(alpha) ∈ ℕ ⟶ ℕ BY ProveWfLemma)) }

1
1. alpha : ℕ ⟶ ℕ
2. make-strict(alpha) ∈ ℕ ⟶ ℕ
⊢ make-strict(alpha) ∈ StrictInc

---

Latex:

---

Latex:
\mforall{}[alpha:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  (make-strict(alpha)  \mmember{}  StrictInc)


By

---

Latex:
(Auto  THEN  (Assert  make-strict(alpha)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  BY  ProveWfLemma))

---

Home Index