---

Step * 1 of Lemma deq-sub-bag_wf

.....equality..... 
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
⊢ 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
BY
{ SqequalBySymbComp200 }

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  as  :  bag(T)
4.  bs  :  bag(T)
\mvdash{}  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


By

---

Latex:
SqequalBySymbComp200

---

Home Index