Step
*
of Lemma
not-not-sig-to-W-implies-stable
∀[A:Type]. ((∀[B:A ⟶ Type]. ((¬¬(a:A × (¬B[a])))
⇒ W(A;a.B[a])))
⇒ Stable{A})
BY
{ (Auto THEN (D 0 THENA Auto)) }
1
1. [A] : Type
2. ∀[B:A ⟶ Type]. ((¬¬(a:A × (¬B[a])))
⇒ W(A;a.B[a]))@i'
3. ¬¬A
⊢ A
Latex:
Latex:
\mforall{}[A:Type]. ((\mforall{}[B:A {}\mrightarrow{} Type]. ((\mneg{}\mneg{}(a:A \mtimes{} (\mneg{}B[a]))) {}\mRightarrow{} W(A;a.B[a]))) {}\mRightarrow{} Stable\{A\})
By
Latex:
(Auto THEN (D 0 THENA Auto))
Home
Index