---

Step * 1 of Lemma bag-count-drop-trivial


1. T : Type
2. eq : EqDecider(T)
3. x : T
4. y : T
5. bs : bag(T)
6. ¬(x = y ∈ T)
7. as : bag(T)
8. bs = ({x} + as) ∈ bag(T)
9. bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?)
⊢ (#y in {x}) = 0 ∈ ℕ
BY
{ (RW (SubC (TagC (mk_tag_term 100))) 0 THEN AutoBoolCase ⌜eq y x⌝⋅) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  y  :  T
5.  bs  :  bag(T)
6.  \mneg{}(x  =  y)
7.  as  :  bag(T)
8.  bs  =  (\{x\}  +  as)
9.  bag-remove1(eq;bs;x)  =  (inl  as)
\mvdash{}  (\#y  in  \{x\})  =  0


By

---

Latex:
(RW  (SubC  (TagC  (mk\_tag\_term  100)))  0  THEN  AutoBoolCase  \mkleeneopen{}eq  y  x\mkleeneclose{}\mcdot{})

---

Home Index