---

Step * 1 of Lemma mset_map_id


∀s:DSet. ∀a:|s| List.  (map(Id{|s|};a) ≡(|s|) a)
BY
{ ((RepD THENM StrengthenRel) THENA Auto) }

1
1. s : DSet
2. a : |s| List
⊢ map(Id{|s|};a) = a ∈ (|s| List)

---

Latex:

---

Latex:

\mforall{}s:DSet.  \mforall{}a:|s|  List.    (map(Id\{|s|\};a)  \mequiv{}(|s|)  a)


By

---

Latex:
((RepD  THENM  StrengthenRel)  THENA  Auto)

---

Home Index