---

Step * 1 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'
6. R : Type@i'
7. (a:A × (B[a] ⇒ R)) ⇒ R@i
⊢ a:A × (B[a] ⇒ R)
BY
{ (RenameVar `g' (-3) THEN RenameVar `x' (-1) THEN UseWitness ⌜<a, λb.(g b R x)>⌝⋅ THEN MemCD THEN Auto) }

---

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'
6.  R  :  Type@i'
7.  (a:A  \mtimes{}  (B[a]  {}\mRightarrow{}  R))  {}\mRightarrow{}  R@i
\mvdash{}  a:A  \mtimes{}  (B[a]  {}\mRightarrow{}  R)


By

---

Latex:
(RenameVar  `g'  (-3)
  THEN  RenameVar  `x'  (-1)
  THEN  UseWitness  \mkleeneopen{}<a,  \mlambda{}b.(g  b  R  x)>\mkleeneclose{}\mcdot{}
  THEN  MemCD
  THEN  Auto)

---

Home Index