---

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