---

Step * 1 of Lemma make-strict_wf


1. alpha : ℕ ⟶ ℕ
2. make-strict(alpha) ∈ ℕ ⟶ ℕ
⊢ make-strict(alpha) ∈ StrictInc
BY
{ xxx(BLemma `implies-strict-inc` THEN Auto)xxx }

1
1. alpha : ℕ ⟶ ℕ
2. make-strict(alpha) ∈ ℕ ⟶ ℕ
3. i : ℕ
⊢ make-strict(alpha) i < make-strict(alpha) (i + 1)

---

Latex:

---

Latex:

1.  alpha  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  make-strict(alpha)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  make-strict(alpha)  \mmember{}  StrictInc


By

---

Latex:
xxx(BLemma  `implies-strict-inc`  THEN  Auto)xxx

---

Home Index