---

Step * 1 1 1 of Lemma param-co-W-ext


1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. X : ℕ ⟶ P ⟶ Type
6. p : P
7. x : ⋂n:ℕ. (a:A[p] × (b:B[p;a] ⟶ (X n C[p;a;b])))
8. x ~ <fst(x), snd(x)>
9. fst(x) ∈ A[p]
⊢ snd(x) ∈ b:B[p;fst(x)] ⟶ (⋂n:ℕ. (X n C[p;fst(x);b]))
BY
{ (ExtWith [`b'] [⌜Top⌝]⋅⋅
   THEN Auto
   THEN With ⌜n⌝ (DVar `x')⋅
   THEN Auto
   THEN (GenConcl ⌜x = z ∈ (a:A[p] × (b:B[p;a] ⟶ (X n C[p;a;b])))⌝⋅ THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:

1.  P  :  Type
2.  A  :  P  {}\mrightarrow{}  Type
3.  B  :  p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type
4.  C  :  p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P
5.  X  :  \mBbbN{}  {}\mrightarrow{}  P  {}\mrightarrow{}  Type
6.  p  :  P
7.  x  :  \mcap{}n:\mBbbN{}.  (a:A[p]  \mtimes{}  (b:B[p;a]  {}\mrightarrow{}  (X  n  C[p;a;b])))
8.  x  \msim{}  <fst(x),  snd(x)>
9.  fst(x)  \mmember{}  A[p]
\mvdash{}  snd(x)  \mmember{}  b:B[p;fst(x)]  {}\mrightarrow{}  (\mcap{}n:\mBbbN{}.  (X  n  C[p;fst(x);b]))


By

---

Latex:
(ExtWith  [`b']  [\mkleeneopen{}Top\mkleeneclose{}]\mcdot{}\mcdot{}
  THEN  Auto
  THEN  With  \mkleeneopen{}n\mkleeneclose{}  (DVar  `x')\mcdot{}
  THEN  Auto
  THEN  (GenConcl  \mkleeneopen{}x  =  z\mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index