Step
*
of Lemma
ite_rw_test
∀[n:ℕ]. ∀[i:ℕ+n].  False supposing (¬(0 = 0 ∈ ℤ)) ∧ (¬(n = 0 ∈ ℤ))
BY
{ Auto }
Latex:
Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[i:\mBbbN{}\msupplus{}n].    False  supposing  (\mneg{}(0  =  0))  \mwedge{}  (\mneg{}(n  =  0))
By
Latex:
Auto
Home
Index