---

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


1. A : Type
2. B : A ⟶ Type
3. ∀R:Type. (((a:A × (B[a] ⇒ R)) ⇒ R) ⇒ R)
⊢ W(A;a.B[a])
BY
{ (InstHyp [⌜W(A;a.B[a])⌝] (-1)⋅ THEN Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(InstHyp  [\mkleeneopen{}W(A;a.B[a])\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)

---

Home Index