---

Step * 1 1 1 1 1 1 of Lemma mset_ind_a


1. s : DSet
2. Q : MSet{s} ⟶ ℙ
3. Q[[]]
4. ∀x:|s|. Q[mset_inj{s}(x)]
5. ∀ys,ys':MSet{s}.  (Q[ys] ⇒ Q[ys'] ⇒ Q[ys + ys'])
6. u : |s|
7. v : |s| List
8. Q[v]
9. Q[mset_inj{s}(u) + v]
⊢ Q[[u / v]]
BY
{ RepUnfolds ``mset_inj mset_sum mk_mset`` (-1)
THEN AbReduce (-1) }

1
1. s : DSet
2. Q : MSet{s} ⟶ ℙ
3. Q[[]]
4. ∀x:|s|. Q[mset_inj{s}(x)]
5. ∀ys,ys':MSet{s}.  (Q[ys] ⇒ Q[ys'] ⇒ Q[ys + ys'])
6. u : |s|
7. v : |s| List
8. Q[v]
9. Q[[u / v]]
⊢ Q[[u / v]]

---

Latex:

---

Latex:

1.  s  :  DSet
2.  Q  :  MSet\{s\}  {}\mrightarrow{}  \mBbbP{}
3.  Q[[]]
4.  \mforall{}x:|s|.  Q[mset\_inj\{s\}(x)]
5.  \mforall{}ys,ys':MSet\{s\}.    (Q[ys]  {}\mRightarrow{}  Q[ys']  {}\mRightarrow{}  Q[ys  +  ys'])
6.  u  :  |s|
7.  v  :  |s|  List
8.  Q[v]
9.  Q[mset\_inj\{s\}(u)  +  v]
\mvdash{}  Q[[u  /  v]]


By

---

Latex:
RepUnfolds  ``mset\_inj  mset\_sum  mk\_mset``  (-1)
THEN  AbReduce  (-1)

---

Home Index