Step * 1 1 of Lemma list-diff-diff


1. Type
2. eq EqDecider(T)
3. as List
4. bs List
5. cs List
6. T@i
7. (t ∈ as)@i
⊢ (t ∈ bs)) ∧ (t ∈ cs)) ⇐⇒ ¬((t ∈ bs) ∨ (t ∈ cs))
BY
Auto }


Latex:


Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  as  :  T  List
4.  bs  :  T  List
5.  cs  :  T  List
6.  t  :  T@i
7.  (t  \mmember{}  as)@i
\mvdash{}  (\mneg{}(t  \mmember{}  bs))  \mwedge{}  (\mneg{}(t  \mmember{}  cs))  \mLeftarrow{}{}\mRightarrow{}  \mneg{}((t  \mmember{}  bs)  \mvee{}  (t  \mmember{}  cs))


By


Latex:
Auto




Home Index