---

Step * of Lemma diff_wf

∀s:DSet. ∀as,bs:|s| List.  (as - bs ∈ |s| List)
BY
{ ((UnivCD THENA Auto) THEN MoveToConcl (-2) THEN ListInd (-1) THEN RecCaseSplit `diff` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}as,bs:|s|  List.    (as  -  bs  \mmember{}  |s|  List)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  MoveToConcl  (-2)  THEN  ListInd  (-1)  THEN  RecCaseSplit  `diff`  THEN  Auto)

---

Home Index