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