---

Step * of Lemma bag_remove1_aux_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs,checked:T List].  (bag_remove1_aux(eq;checked;x;bs) ∈ T List?)
BY
{ (InductionOnList THEN RecUnfold `bag_remove1_aux` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[bs,checked:T  List].
    (bag\_remove1\_aux(eq;checked;x;bs)  \mmember{}  T  List?)


By

---

Latex:
(InductionOnList  THEN  RecUnfold  `bag\_remove1\_aux`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index