---

Step * 1 1 of Lemma mset_mon_for_elim


1. s : DSet
2. T : Type
3. f : T ⟶ (|s| List)
⊢ 0{s} = mk_mset([]) ∈ MSet{s}
BY
{ (RWH null_mset_elimC 0 THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  T  :  Type
3.  f  :  T  {}\mrightarrow{}  (|s|  List)
\mvdash{}  0\{s\}  =  mk\_mset([])


By

---

Latex:
(RWH  null\_mset\_elimC  0  THEN  Auto)

---

Home Index