Step
*
of Lemma
test2
∀p:ℕ + (ℕ ⟶ ℕ). ∀bs:ℕ List. (case p of inl(x) => x + 1 | inr(y) => y 3 ∈ ℤ)
BY
{ Auto }
Latex:
Latex:
\mforall{}p:\mBbbN{} + (\mBbbN{} {}\mrightarrow{} \mBbbN{}). \mforall{}bs:\mBbbN{} List. (case p of inl(x) => x + 1 | inr(y) => y 3 \mmember{} \mBbbZ{})
By
Latex:
Auto
Home
Index