---

Step * of Lemma insert-not-nil

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[L:T List].  (¬(insert(a;L) = [] ∈ (T List)))
BY
{ (Auto THEN (D 0 THENA Auto) THEN Unfold `insert` -1) }

1
1. T : Type
2. eq : EqDecider(T)
3. a : T
4. L : T List
5. eval x = eval_list(L) in if a ∈b x then x else [a / x] fi  = [] ∈ (T List)
⊢ False

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[a:T].  \mforall{}[L:T  List].    (\mneg{}(insert(a;L)  =  []))


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  Unfold  `insert`  -1)

---

Home Index