Step
*
1
2
of Lemma
bag-append-union
1. T : Type
2. bs : bag(bag(T))
3. u : bag(T)
4. v : bag(T) List
5. bag-union(v + bs) = (bag-union(v) + bag-union(bs)) ∈ bag(T)
⊢ (u @ bag-union(v @ bs)) = ((u @ bag-union(v)) @ bag-union(bs)) ∈ bag(T)
BY
{ (Fold `bag-append` 0 THEN HypSubst' (-1) 0 THEN Auto) }
Latex:
Latex:
1. T : Type
2. bs : bag(bag(T))
3. u : bag(T)
4. v : bag(T) List
5. bag-union(v + bs) = (bag-union(v) + bag-union(bs))
\mvdash{} (u @ bag-union(v @ bs)) = ((u @ bag-union(v)) @ bag-union(bs))
By
Latex:
(Fold `bag-append` 0 THEN HypSubst' (-1) 0 THEN Auto)
Home
Index