---

Step * of Lemma ml_insert_int-sq

∀[l:ℤ List]. ∀[x:ℤ].  (ml_insert_int(x;l) ~ insert-int(x;l))
BY
{ ((InductionOnList THEN Intro) THEN UseWitness ⌜Ax⌝⋅ THEN MemCD) }

1
.....eq aux..... 
1. x : ℤ
⊢ ml_insert_int(x;[]) ~ insert-int(x;[])

2
.....eq aux..... 
1. u : ℤ
2. v : ℤ List
3. ∀[x:ℤ]. (ml_insert_int(x;v) ~ insert-int(x;v))
4. x : ℤ
⊢ ml_insert_int(x;[u / v]) ~ insert-int(x;[u / v])

---

Latex:

---

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


By

---

Latex:
((InductionOnList  THEN  Intro)  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  MemCD)

---

Home Index