---

Step * 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. a:A × (B[a] ⇒ W(A;a.B[a]))
⊢ W(A;a.B[a])
BY
{ (RenameVar `p' (-1)⋅ THEN UseWitness ⌜p⌝⋅ THEN Auto) }

1
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])

---

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


By

---

Latex:
(RenameVar  `p'  (-1)\mcdot{}  THEN  UseWitness  \mkleeneopen{}p\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index