---

Step * of Lemma length-list-diff

∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List.  ((||as-bs|| ≤ ||as||) ∧ ||as-bs|| < ||as|| supposing (∃a∈as. (a ∈ bs)))
BY
{ (Unfold `list-diff` 0 THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. bs : T List
5. ||filter(λa.(¬ba ∈b bs);as)|| ≤ ||as||
6. (∃a∈as. (a ∈ bs))
⊢ ||filter(λa.(¬ba ∈b bs);as)|| < ||as||

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}as,bs:T  List.
        ((||as-bs||  \mleq{}  ||as||)  \mwedge{}  ||as-bs||  <  ||as||  supposing  (\mexists{}a\mmember{}as.  (a  \mmember{}  bs)))


By

---

Latex:
(Unfold  `list-diff`  0  THEN  Auto)

---

Home Index