---

Step * of Lemma dset_list_wf

∀s:DSet. (s List ∈ DSet)
BY
{ (Unfold `dset_list` 0 THEN Auto THEN D 0 THEN Reduce 0 THEN Auto) }

1
1. s : DSet@i'
2. x : |s| List
3. y : |s| List
4. ↑(x =b y)
⊢ x = y ∈ (|s| List)

2
1. s : DSet@i'
2. x : |s| List
3. y : |s| List
4. x = y ∈ (|s| List)
⊢ ↑(x =b y)

---

Latex:

---

Latex:
\mforall{}s:DSet.  (s  List  \mmember{}  DSet)


By

---

Latex:
(Unfold  `dset\_list`  0  THEN  Auto  THEN  D  0  THEN  Reduce  0  THEN  Auto)

---

Home Index