Step
*
of Lemma
bag-member-union
∀[T:Type]. ∀[x:T]. ∀[bbs:bag(bag(T))]. uiff(x ↓∈ bag-union(bbs);↓∃b:bag(T). (x ↓∈ b ∧ b ↓∈ bbs))
BY
{ ((UnivCD THENA Auto) THEN (BagToList (-1) THENA Auto)) }
1
1. T : Type
2. x : T
3. bbs : bag(T) List
⊢ uiff(x ↓∈ bag-union(bbs);↓∃b:bag(T). (x ↓∈ b ∧ b ↓∈ bbs))
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[x:T]. \mforall{}[bbs:bag(bag(T))]. uiff(x \mdownarrow{}\mmember{} bag-union(bbs);\mdownarrow{}\mexists{}b:bag(T). (x \mdownarrow{}\mmember{} b \mwedge{} b \mdownarrow{}\mmember{} bbs))
By
Latex:
((UnivCD THENA Auto) THEN (BagToList (-1) THENA Auto))
Home
Index