---

Step * 1 1 of Lemma mset_fact


1. s : DSet
⊢ ∀a:|s| List. (a ≡(|s|) (For{<s List, @>} x ∈ a. [x]))
BY
{ ((D 0) THENA Auto) 
THEN ((StrengthenRel THENM BLemma `lapp_fact`) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
\mvdash{}  \mforall{}a:|s|  List.  (a  \mequiv{}(|s|)  (For\{<s  List,  @>\}  x  \mmember{}  a.  [x]))


By

---

Latex:
((D  0)  THENA  Auto) 
THEN  ((StrengthenRel  THENM  BLemma  `lapp\_fact`)  THEN  Auto)

---

Home Index