---

Step * 2 of Lemma dset_list_wf


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

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO  "assert\_of\_eq\_list"  0  THEN  Auto)\mcdot{}

---

Home Index