---

Step * 1 of Lemma dset_list_wf


1. s : DSet@i'
2. x : |s| List
3. y : |s| List
4. ↑(x =b y)
⊢ x = y ∈ (|s| List)
BY
{ (RWO "assert_of_eq_list" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet@i'
2.  x  :  |s|  List
3.  y  :  |s|  List
4.  \muparrow{}(x  =\msubb{}  y)
\mvdash{}  x  =  y


By

---

Latex:
(RWO  "assert\_of\_eq\_list"  (-1)  THEN  Auto)

---

Home Index