---

Step * of Lemma sq_stable__all

∀[A:Type]. ∀[P:A ⟶ ℙ].  ((∀x:A. SqStable(P[x])) ⇒ SqStable(∀x:A. P[x]))
BY
{ ((Unfold `sq_stable` 0 THEN UnivCD) 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:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x:A.  SqStable(P[x]))  {}\mRightarrow{}  SqStable(\mforall{}x:A.  P[x]))


By

---

Latex:
((Unfold  `sq\_stable`  0  THEN  UnivCD)  THENA  Auto)

---

Home Index