---

Step * of Lemma list-diff-cons-single

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as:T List]. ∀[b,x:T].  [x / as]-[b] = [x / as-[b]] ∈ (T List) supposing ¬(x = b ∈ T)
BY
{ (Auto THEN (RWO  "list-diff-cons" 0 THENA Auto) THEN AutoSplit) }

1
1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. b : T
5. x : T
6. ¬(x = b ∈ T)
7. (x ∈ [b])
⊢ as-[b] = [x / as-[b]] ∈ (T List)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[as:T  List].  \mforall{}[b,x:T].
    [x  /  as]-[b]  =  [x  /  as-[b]]  supposing  \mneg{}(x  =  b)


By

---

Latex:
(Auto  THEN  (RWO    "list-diff-cons"  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index