---

Step * of Lemma deq-sub-bag_wf

No Annotations
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].  (deq-sub-bag(eq;as;bs) ∈ 𝔹)
BY
{ ((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)
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

2
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
⊢ case TERMOF{decidable__sub-bag:o, \\v:l, i:l} deq-witness(eq) as bs of inl(x) => tt | inr(x) => ff ∈ 𝔹

---

Latex:

---

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


By

---

Latex:
((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