---

Step * of Lemma assert-deq-sub-bag

No Annotations
∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:bag(T).  (↑deq-sub-bag(eq;as;bs) ⇐⇒ sub-bag(T;as;bs))
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN Unfold `deq-sub-bag` 0
          THEN Subst' TERMOF{decidable__sub-bag:o, 1:l, 1:l} deq-witness(eq) as bs ~ TERMOF{decidable__sub-bag:o,
                                                                                            \\v:l,
                                                                                            i:l} 
                                                                                     deq-witness(eq) 
                                                                                     as 
                                                                                     bs 0) }

1
.....equality..... 
1. T : Type
2. eq : EqDecider(T)@i
3. as : bag(T)@i
4. bs : bag(T)@i
⊢ TERMOF{decidable__sub-bag:o, 1:l, 1:l} deq-witness(eq) as bs ~ TERMOF{decidable__sub-bag:o, \\v:l, i:l} 
                                                                 deq-witness(eq) 
                                                                 as 
                                                                 bs

2
1. [T] : Type
2. eq : EqDecider(T)@i
3. as : bag(T)@i
4. bs : bag(T)@i
⊢ ↑case TERMOF{decidable__sub-bag:o, \\v:l, i:l} deq-witness(eq) as bs of inl(x) => tt | inr(x) => ff
⇐⇒ sub-bag(T;as;bs)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}as,bs:bag(T).    (\muparrow{}deq-sub-bag(eq;as;bs)  \mLeftarrow{}{}\mRightarrow{}  sub-bag(T;as;bs))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  Unfold  `deq-sub-bag`  0
                THEN  Subst'  TERMOF\{decidable\_\_sub-bag:o,  1:l,  1:l\}  deq-witness(eq)  as  bs 
                \msim{}  TERMOF\{decidable\_\_sub-bag:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  deq-witness(eq)  as  bs  0)

---

Home Index