---

Step * 1 1 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)
4. p : a:A × (B[a] ⇒ W(A;a.B[a]))
⊢ p ∈ W(A;a.B[a])
BY
{ TACTIC:(DWtype 0 THEN Auto) }

---

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)
4.  p  :  a:A  \mtimes{}  (B[a]  {}\mRightarrow{}  W(A;a.B[a]))
\mvdash{}  p  \mmember{}  W(A;a.B[a])


By

---

Latex:
TACTIC:(DWtype  0  THEN  Auto)

---

Home Index