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