---

Step * of Lemma b_all-cons

∀[B:Type]. ∀b:bag(B). ∀P:B ⟶ ℙ. ∀x:B.  ((∀b:B. SqStable(P[b])) ⇒ (b_all(B;x.b;x.P[x]) ⇐⇒ P[x] ∧ b_all(B;b;x.P[x])))
BY
{ Auto }

1
1. [B] : Type
2. b : bag(B)
3. P : B ⟶ ℙ
4. x : B
5. ∀b:B. SqStable(P[b])
6. b_all(B;x.b;x.P[x])
⊢ P[x]

2
1. [B] : Type
2. b : bag(B)
3. P : B ⟶ ℙ
4. x : B
5. ∀b:B. SqStable(P[b])
6. b_all(B;x.b;x.P[x])
⊢ b_all(B;b;x.P[x])

3
1. [B] : Type
2. b : bag(B)
3. P : B ⟶ ℙ
4. x : B
5. ∀b:B. SqStable(P[b])
6. P[x]
7. b_all(B;b;x.P[x])
⊢ b_all(B;x.b;x.P[x])

---

Latex:

---

Latex:
\mforall{}[B:Type]
    \mforall{}b:bag(B).  \mforall{}P:B  {}\mrightarrow{}  \mBbbP{}.  \mforall{}x:B.
        ((\mforall{}b:B.  SqStable(P[b]))  {}\mRightarrow{}  (b\_all(B;x.b;x.P[x])  \mLeftarrow{}{}\mRightarrow{}  P[x]  \mwedge{}  b\_all(B;b;x.P[x])))


By

---

Latex:
Auto

---

Home Index