---

Step * of Lemma list-diff-property

∀[T:Type]
  ∀eq:EqDecider(T). ∀as,bs:T List.
    ((∀x:T. ((x ∈ as-bs) ⇐⇒ (x ∈ as) ∧ (¬(x ∈ bs)))) ∧ no_repeats(T;as-bs) supposing no_repeats(T;as))
BY
{ ((UnivCD THENA Auto) THEN D 0) }

1
1. [T] : Type
2. eq : EqDecider(T)@i
3. as : T List@i
4. bs : T List@i
⊢ ∀x:T. ((x ∈ as-bs) ⇐⇒ (x ∈ as) ∧ (¬(x ∈ bs)))

2
1. [T] : Type
2. eq : EqDecider(T)@i
3. as : T List@i
4. bs : T List@i
⊢ no_repeats(T;as-bs) supposing no_repeats(T;as)

---

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))))
        \mwedge{}  no\_repeats(T;as-bs)  supposing  no\_repeats(T;as))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  0)

---

Home Index