---

Step * 3 of Lemma b_all-map2

.....wf..... 
1. A : Type
2. B : Type
3. b : bag(A)
4. f : {a:A| a ↓∈ b}  ⟶ B
5. P : B ⟶ ℙ
6. ∀b:B. SqStable(P[b])
⊢ istype(b_all(A;b;x.P[f x]))
BY
{ (InstLemma `b_all-wf2` [⌜A⌝;⌜b⌝;⌜λ2x.P[f x]⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  A  :  Type
2.  B  :  Type
3.  b  :  bag(A)
4.  f  :  \{a:A|  a  \mdownarrow{}\mmember{}  b\}    {}\mrightarrow{}  B
5.  P  :  B  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}b:B.  SqStable(P[b])
\mvdash{}  istype(b\_all(A;b;x.P[f  x]))


By

---

Latex:
(InstLemma  `b\_all-wf2`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.P[f  x]\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index