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