Step
*
1
1
1
2
of Lemma
bag-member-parts'
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. x : T
5. bs : bag(T)
6. L : bag(T) List+
7. bs = {} ∈ bag(T)
8. bs ~ {}
9. L = [{}] ∈ bag(T) List+
⊢ (∀x∈tl(L).¬(x = {} ∈ bag(T)))
BY
{ xxx((HypSubst (-1) 0 THEN Reduce 0) THEN Auto)xxx }
Latex:
Latex:
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. x : T
5. bs : bag(T)
6. L : bag(T) List\msupplus{}
7. bs = \{\}
8. bs \msim{} \{\}
9. L = [\{\}]
\mvdash{} (\mforall{}x\mmember{}tl(L).\mneg{}(x = \{\}))
By
Latex:
xxx((HypSubst (-1) 0 THEN Reduce 0) THEN Auto)xxx
Home
Index