---

Step * 1 of Lemma mset_inj_wf


1. s : DSet@i'
2. x : |s|@i
⊢ mset_inj{s}(x) ∈ MSet{s}
BY
{ ((Unfold `mset_inj` 0) THEN Auto) 
 }

---

Latex:

---

Latex:

1.  s  :  DSet@i'
2.  x  :  |s|@i
\mvdash{}  mset\_inj\{s\}(x)  \mmember{}  MSet\{s\}


By

---

Latex:
((Unfold  `mset\_inj`  0)  THEN  Auto) 

---

Home Index