---

Step * of Lemma list-diff-disjoint

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:T List].  as-bs = as ∈ (T List) supposing l_disjoint(T;as;bs)
BY
{ (InductionOnList
   THEN Try ((Unfold `list-diff` 0 THEN Reduce 0 THEN Complete (Auto)))
   THEN RepeatFor 2 (ParallelLast)) }

1
.....antecedent..... 
1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. ∀[bs:T List]. v-bs = v ∈ (T List) supposing l_disjoint(T;v;bs)
6. bs : T List
7. l_disjoint(T;[u / v];bs)
⊢ l_disjoint(T;v;bs)

2
1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. ∀[bs:T List]. v-bs = v ∈ (T List) supposing l_disjoint(T;v;bs)
6. bs : T List
7. l_disjoint(T;[u / v];bs)
8. v-bs = v ∈ (T List)
⊢ [u / v]-bs = [u / v] ∈ (T List)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[as,bs:T  List].    as-bs  =  as  supposing  l\_disjoint(T;as;bs)


By

---

Latex:
(InductionOnList
  THEN  Try  ((Unfold  `list-diff`  0  THEN  Reduce  0  THEN  Complete  (Auto)))
  THEN  RepeatFor  2  (ParallelLast))

---

Home Index