---

Step * of Lemma list-diff-diff

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs,cs:T List].  (as-bs-cs = as-bs @ cs ∈ (T List))
BY
{ ((Unfold `list-diff` 0 THEN Auto)
   THEN (RWO "filter-filter" 0 THENA Auto)
   THEN Reduce 0
   THEN RepeatFor 2 ((EqCD THEN Auto))) }

1
.....subterm..... T:t
1:n
1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. bs : T List
5. cs : T List
6. t : {x:T| (x ∈ as)} @i
⊢ (¬bt ∈b bs) ∧b (¬bt ∈b cs) = ¬bt ∈b bs @ cs

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[as,bs,cs:T  List].    (as-bs-cs  =  as-bs  @  cs)


By

---

Latex:
((Unfold  `list-diff`  0  THEN  Auto)
  THEN  (RWO  "filter-filter"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index