Step
*
of Lemma
ml_insert_int_wf
∀[l:ℤ List]. ∀[x:ℤ]. (ml_insert_int(x;l) ∈ ℤ List)
BY
{ (Auto THEN RWO "ml_insert_int-sq" 0 THEN Auto) }
Latex:
Latex:
\mforall{}[l:\mBbbZ{} List]. \mforall{}[x:\mBbbZ{}]. (ml\_insert\_int(x;l) \mmember{} \mBbbZ{} List)
By
Latex:
(Auto THEN RWO "ml\_insert\_int-sq" 0 THEN Auto)
Home
Index