Step
*
1
of Lemma
sq_stable__all
1. [A] : Type
2. [P] : A ⟶ ℙ
3. ∀x:A. ((↓P[x])
⇒ P[x])
4. ↓∀x:A. P[x]
5. x : A
⊢ P[x]
BY
{ (BackThruHyp 3 THENA Auto) }
1
1. [A] : Type
2. [P] : A ⟶ ℙ
3. ∀x:A. ((↓P[x])
⇒ P[x])
4. ↓∀x:A. P[x]
5. x : A
⊢ ↓P[x]
Latex:
Latex:
1. [A] : Type
2. [P] : A {}\mrightarrow{} \mBbbP{}
3. \mforall{}x:A. ((\mdownarrow{}P[x]) {}\mRightarrow{} P[x])
4. \mdownarrow{}\mforall{}x:A. P[x]
5. x : A
\mvdash{} P[x]
By
Latex:
(BackThruHyp 3 THENA Auto)
Home
Index