Step
*
of Lemma
bag-eq-subtype
∀[A:Type]. ∀[d1,d2:bag(A)]. d1 = d2 ∈ bag({a:A| a ↓∈ d1} ) supposing d1 = d2 ∈ bag(A)
BY
{ ((UnivCD THENA Auto)
THEN InstLemma `bag-eq-subtype1` [⌜A⌝;⌜λa.a ↓∈ d1⌝;⌜d1⌝;⌜d2⌝]⋅
THEN All (RepUR ``so_apply``)
THEN Auto
THEN Try (Complete ((BLemma `bag-subtype` THEN Auto)))
THEN (InstLemma `bag-subtype` [⌜A⌝;⌜d2⌝]⋅ THENA Auto)
THEN (Assert ⌜{x:A| x ↓∈ d2} = {a:A| a ↓∈ d1} ∈ Type⌝⋅ THENA (HypSubst' (-2) 0 THEN Auto))
THEN RWO "-1" (-2)
THEN Auto) }
Latex:
Latex:
\mforall{}[A:Type]. \mforall{}[d1,d2:bag(A)]. d1 = d2 supposing d1 = d2
By
Latex:
((UnivCD THENA Auto)
THEN InstLemma `bag-eq-subtype1` [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}a.a \mdownarrow{}\mmember{} d1\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{};\mkleeneopen{}d2\mkleeneclose{}]\mcdot{}
THEN All (RepUR ``so\_apply``)
THEN Auto
THEN Try (Complete ((BLemma `bag-subtype` THEN Auto)))
THEN (InstLemma `bag-subtype` [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}d2\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (Assert \mkleeneopen{}\{x:A| x \mdownarrow{}\mmember{} d2\} = \{a:A| a \mdownarrow{}\mmember{} d1\} \mkleeneclose{}\mcdot{} THENA (HypSubst' (-2) 0 THEN Auto))
THEN RWO "-1" (-2)
THEN Auto)
Home
Index