Step
*
1
of Lemma
W-to-not-not-sig2
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)
BY
{ (RenameVar `w' (-1) THEN MoveToConcl (-1) THEN UseWInductionLemma') }
1
1. A : Type@i'
2. B : A ⟶ Type@i'
3. a : A@i
4. f : B[a] ⟶ W(A;a.B[a])@i
5. ∀b:B[a]. ∀R:Type. (((a:A × (B[a]
⇒ R))
⇒ R)
⇒ R)@i'
⊢ ∀R:Type. (((a:A × (B[a]
⇒ R))
⇒ R)
⇒ R)
Latex:
Latex:
1. A : Type@i'
2. B : A {}\mrightarrow{} Type@i'
3. W(A;a.B[a])@i
\mvdash{} \mforall{}R:Type. (((a:A \mtimes{} (B[a] {}\mRightarrow{} R)) {}\mRightarrow{} R) {}\mRightarrow{} R)
By
Latex:
(RenameVar `w' (-1) THEN MoveToConcl (-1) THEN UseWInductionLemma')
Home
Index