---

Step * of Lemma insert-cases

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[L:T List].
  (insert(a;L) ~ L supposing (a ∈ L) ∧ insert(a;L) ~ [a / L] supposing ¬(a ∈ L))
BY
{ RepeatFor 4 ((D 0 THENA Auto))
THEN (Unfold `insert` 0 THEN (RWO "eval_list_sq" 0 THENA Auto) THEN (CallByValueReduce 0 THENA Auto))
THEN (SplitOnConclITE THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[a:T].  \mforall{}[L:T  List].
    (insert(a;L)  \msim{}  L  supposing  (a  \mmember{}  L)  \mwedge{}  insert(a;L)  \msim{}  [a  /  L]  supposing  \mneg{}(a  \mmember{}  L))


By

---

Latex:
RepeatFor  4  ((D  0  THENA  Auto))
THEN  (Unfold  `insert`  0
            THEN  (RWO  "eval\_list\_sq"  0  THENA  Auto)
            THEN  (CallByValueReduce  0  THENA  Auto))
THEN  (SplitOnConclITE  THEN  Auto)

---

Home Index