---

Step * of Lemma extend-injection_wf

∀[a:ℕ]. ∀[f:ℕa →⟶ ℕa]. ∀[b:{a...}].  (extend-injection(a;f) ∈ ℕb →⟶ ℕb)
BY
{ ProveWfLemma }

1
1. a : ℕ
2. f : ℕa →⟶ ℕa
3. b : {a...}
⊢ λx.if x <z a then f x else x fi  ∈ ℕb →⟶ ℕb

---

Latex:

---

Latex:
\mforall{}[a:\mBbbN{}].  \mforall{}[f:\mBbbN{}a  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}a].  \mforall{}[b:\{a...\}].    (extend-injection(a;f)  \mmember{}  \mBbbN{}b  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}b)


By

---

Latex:
ProveWfLemma

---

Home Index