---

Step * of Lemma not-not-sig-to-W

∀A:Type. ∀B:A ⟶ Type.  ((∀R:Type. (((a:A × (B[a] ⇒ R)) ⇒ R) ⇒ R)) ⇒ W(A;a.B[a]))
BY
{ Auto }

1
1. A : Type
2. B : A ⟶ Type
3. ∀R:Type. (((a:A × (B[a] ⇒ R)) ⇒ R) ⇒ R)
⊢ W(A;a.B[a])

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}B:A  {}\mrightarrow{}  Type.    ((\mforall{}R:Type.  (((a:A  \mtimes{}  (B[a]  {}\mRightarrow{}  R))  {}\mRightarrow{}  R)  {}\mRightarrow{}  R))  {}\mRightarrow{}  W(A;a.B[a]))


By

---

Latex:
Auto

---

Home Index