---

Step * of Lemma nat-star-retract-id

∀[s:ℕ*]. (nat-star-retract(s) = s ∈ ℕ*)
BY
{ (Auto THEN (Assert nat-star-retract(s) ∈ ℕ* BY Auto)) }

1
1. s : ℕ*
2. nat-star-retract(s) ∈ ℕ*
⊢ nat-star-retract(s) = s ∈ ℕ*

---

Latex:

---

Latex:
\mforall{}[s:\mBbbN{}*].  (nat-star-retract(s)  =  s)


By

---

Latex:
(Auto  THEN  (Assert  nat-star-retract(s)  \mmember{}  \mBbbN{}*  BY  Auto))

---

Home Index