Step
*
1
1
of Lemma
list-diff-diff
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 ∈ 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