---

Step * of Lemma nat-retractible

retractible(ℕ)
BY
{ TACTIC:((With ⌜λx.if (x) < (0)  then ⊥  else x⌝ (D 0)⋅ THEN Reduce 0) THENW Auto) }

1
(∀x:ℕ. (if (x) < (0)  then ⊥  else x = x ∈ ℕ)) ∧ (∀x:Base. ((if (x) < (0)  then ⊥  else x)↓ ⇒ (x ∈ ℕ)))

---

Latex:

---

Latex:
retractible(\mBbbN{})


By

---

Latex:
TACTIC:((With  \mkleeneopen{}\mlambda{}x.if  (x)  <  (0)    then  \mbot{}    else  x\mkleeneclose{}  (D  0)\mcdot{}  THEN  Reduce  0)  THENW  Auto)

---

Home Index