---

Step * 1 of Lemma mset_ind_a


1. s : DSet
2. Q : MSet{s} ⟶ ℙ
3. ∀w:MSet{s}. SqStable(Q[w])
4. Q[0{s}]
5. ∀x:|s|. Q[mset_inj{s}(x)]
6. ∀ys,ys':MSet{s}.  (Q[ys] ⇒ Q[ys'] ⇒ Q[ys + ys'])
7. zs : MSet{s}
⊢ Q[zs]
BY
{ ((CSquash THENM Thin 3) THENA Auto) }

1
1. s : DSet
2. Q : MSet{s} ⟶ ℙ
3. Q[0{s}]
4. ∀x:|s|. Q[mset_inj{s}(x)]
5. ∀ys,ys':MSet{s}.  (Q[ys] ⇒ Q[ys'] ⇒ Q[ys + ys'])
6. zs : MSet{s}
⊢ ↓Q[zs]

---

Latex:

---

Latex:

1.  s  :  DSet
2.  Q  :  MSet\{s\}  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}w:MSet\{s\}.  SqStable(Q[w])
4.  Q[0\{s\}]
5.  \mforall{}x:|s|.  Q[mset\_inj\{s\}(x)]
6.  \mforall{}ys,ys':MSet\{s\}.    (Q[ys]  {}\mRightarrow{}  Q[ys']  {}\mRightarrow{}  Q[ys  +  ys'])
7.  zs  :  MSet\{s\}
\mvdash{}  Q[zs]


By

---

Latex:
((CSquash  THENM  Thin  3)  THENA  Auto)

---

Home Index