Step
*
of Lemma
bag-combine-unit-right
∀[A:Type]. ∀[bs:bag(A)]. (⋃x∈bs.[x] ~ bs)
BY
{ (Auto
THEN (GenConcl ⌜bs = L ∈ (Top List)⌝⋅
THENA (Auto THEN (DoSubsume THEN Auto) THEN BLemma `bag-subtype-list` THEN Auto)
)
THEN All Thin) }
1
1. L : Top List
⊢ ⋃x∈L.[x] ~ L
Latex:
Latex:
\mforall{}[A:Type]. \mforall{}[bs:bag(A)]. (\mcup{}x\mmember{}bs.[x] \msim{} bs)
By
Latex:
(Auto
THEN (GenConcl \mkleeneopen{}bs = L\mkleeneclose{}\mcdot{}
THENA (Auto THEN (DoSubsume THEN Auto) THEN BLemma `bag-subtype-list` THEN Auto)
)
THEN All Thin)
Home
Index