---

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