---

Step * of Lemma member-list-diff

∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List. ∀x:T.  ((x ∈ as-bs) ⇐⇒ (x ∈ as) ∧ (¬(x ∈ bs)))
BY
{ ((InstLemma `list-diff-property` []) THEN RepeatFor 4 (ParallelLast) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}as,bs:T  List.  \mforall{}x:T.    ((x  \mmember{}  as-bs)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  as)  \mwedge{}  (\mneg{}(x  \mmember{}  bs)))


By

---

Latex:
((InstLemma  `list-diff-property`  [])  THEN  RepeatFor  4  (ParallelLast)  THEN  Auto)

---

Home Index