---

Step * of Lemma stable__all

∀[T:Type]. ∀[P:T ⟶ ℙ].  ((∀x:T. Stable{P[x]}) ⇒ Stable{∀x:T. P[x]})
BY
{ (Auto THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Stable{P[x]}
4. ¬¬(∀x:T. P[x])
5. x : T
⊢ P[x]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x:T.  Stable\{P[x]\})  {}\mRightarrow{}  Stable\{\mforall{}x:T.  P[x]\})


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index