---

Step * of Lemma sq_stable__uall

∀[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