---

Step * 1 of Lemma all_mset_elim


1. s : DSet@i'
2. F : MSet{s} ⟶ ℙ@i'
3. ∀a:MSet{s}. SqStable(F[a])@i
⊢ ∀a:MSet{s}. F[a] ⇐⇒ ∀a:|s| List. F[mk_mset(a)]
BY
{ Unfolds ``mset so_apply mk_mset`` 0  
THEN Sel (-1) (BLemma `all_quot_elim`) 
THEN Try (Fold `mset` 0) THEN Auto }

---

Latex:

---

Latex:

1.  s  :  DSet@i'
2.  F  :  MSet\{s\}  {}\mrightarrow{}  \mBbbP{}@i'
3.  \mforall{}a:MSet\{s\}.  SqStable(F[a])@i
\mvdash{}  \mforall{}a:MSet\{s\}.  F[a]  \mLeftarrow{}{}\mRightarrow{}  \mforall{}a:|s|  List.  F[mk\_mset(a)]


By

---

Latex:
Unfolds  ``mset  so\_apply  mk\_mset``  0   
THEN  Sel  (-1)  (BLemma  `all\_quot\_elim`) 
THEN  Try  (Fold  `mset`  0)  THEN  Auto

---

Home Index