---

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


1. A : Type@i'
2. B : A ⟶ Type@i'
3. a : A@i
4. f : B[a] ⟶ W(A;a.B[a])@i
5. ∀b:B[a]. ∀R:Type.  (((a:A × (B[a] ⇒ R)) ⇒ R) ⇒ R)@i'
⊢ ∀R:Type. (((a:A × (B[a] ⇒ R)) ⇒ R) ⇒ R)
BY
{ (Auto THEN BHyp (-1) ) }

1
1. A : Type@i'
2. B : A ⟶ Type@i'
3. a : A@i
4. f : B[a] ⟶ W(A;a.B[a])@i
5. ∀b:B[a]. ∀R:Type.  (((a:A × (B[a] ⇒ R)) ⇒ R) ⇒ R)@i'
6. R : Type@i'
7. (a:A × (B[a] ⇒ R)) ⇒ R@i
⊢ a:A × (B[a] ⇒ R)

---

Latex:

---

Latex:

1.  A  :  Type@i'
2.  B  :  A  {}\mrightarrow{}  Type@i'
3.  a  :  A@i
4.  f  :  B[a]  {}\mrightarrow{}  W(A;a.B[a])@i
5.  \mforall{}b:B[a].  \mforall{}R:Type.    (((a:A  \mtimes{}  (B[a]  {}\mRightarrow{}  R))  {}\mRightarrow{}  R)  {}\mRightarrow{}  R)@i'
\mvdash{}  \mforall{}R:Type.  (((a:A  \mtimes{}  (B[a]  {}\mRightarrow{}  R))  {}\mRightarrow{}  R)  {}\mRightarrow{}  R)


By

---

Latex:
(Auto  THEN  BHyp  (-1)  )

---

Home Index