Step
*
1
of Lemma
list-diff-diff
.....subterm..... T:t
1:n
1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. bs : T List
5. cs : T List
6. t : {x:T| (x ∈ as)} @i
⊢ (¬bt ∈b bs) ∧b (¬bt ∈b cs) = ¬bt ∈b bs @ cs
BY
{ (D -1 THEN ((BLemma `iff_imp_equal_bool` THENM RW assert_pushdownC 0 THENM RWO "member_append" 0) THENA Auto)) }
1
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))
Latex:
Latex:
.....subterm..... T:t
1:n
1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. bs : T List
5. cs : T List
6. t : \{x:T| (x \mmember{} as)\} @i
\mvdash{} (\mneg{}\msubb{}t \mmember{}\msubb{} bs) \mwedge{}\msubb{} (\mneg{}\msubb{}t \mmember{}\msubb{} cs) = \mneg{}\msubb{}t \mmember{}\msubb{} bs @ cs
By
Latex:
(D -1
THEN ((BLemma `iff\_imp\_equal\_bool` THENM RW assert\_pushdownC 0 THENM RWO "member\_append" 0)
THENA Auto
)
)
Home
Index