---

Step * of Lemma ml-insert-int_wf

∀[l:ℤ List]. ∀[x:ℤ].  (ml-insert-int(x;l) ∈ ℤ List)
BY
{ (InstLemma `ml-insert-int-sq` [] THEN RepeatFor 2 (ParallelLast') THEN HypSubst' (-1) 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[l:\mBbbZ{}  List].  \mforall{}[x:\mBbbZ{}].    (ml-insert-int(x;l)  \mmember{}  \mBbbZ{}  List)


By

---

Latex:
(InstLemma  `ml-insert-int-sq`  []  THEN  RepeatFor  2  (ParallelLast')  THEN  HypSubst'  (-1)  0  THEN  Auto)

---

Home Index