---

Step * of Lemma remove-combine_wf

∀T:Type. ∀cmp:T ⟶ ℤ. ∀l:T List.  (remove-combine(cmp;l) ∈ T List)
BY
{ (InductionOnList THEN RepUR ``remove-combine`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}cmp:T  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}l:T  List.    (remove-combine(cmp;l)  \mmember{}  T  List)


By

---

Latex:
(InductionOnList  THEN  RepUR  ``remove-combine``  0  THEN  Auto)

---

Home Index