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