---

Step * of Lemma bag-drop-no-repeats

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  bag-no-repeats(T;bag-drop(eq;bs;x)) supposing bag-no-repeats(T;bs)
BY
{ (Auto THEN (InstLemma `bag-drop-property` [⌜T⌝;⌜eq⌝;⌜x⌝;⌜bs⌝]⋅ THENA Auto) THEN D (-1) THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. x : T
5. bag-no-repeats(T;bs)
6. bs = ({x} + bag-drop(eq;bs;x)) ∈ bag(T)
⊢ bag-no-repeats(T;bag-drop(eq;bs;x))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x:T].
    bag-no-repeats(T;bag-drop(eq;bs;x))  supposing  bag-no-repeats(T;bs)


By

---

Latex:
(Auto  THEN  (InstLemma  `bag-drop-property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  (-1)  THEN  Auto)

---

Home Index