---

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

.....subterm..... T:t
1:n
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])))
⊢ x ∈ a:A[p] × (b:B[p;a] ⟶ (⋂n:ℕ. (X n C[p;a;b])))
BY
{ ((Assert (x ~ <fst(x), snd(x)>) ∧ (fst(x) ∈ A[p]) BY
          (With ⌜0⌝ (D (-1))⋅
           THEN Auto
           THEN (GenConcl ⌜x = z ∈ (a:A[p] × (b:B[p;a] ⟶ (X 0 C[p;a;b])))⌝⋅ THEN Auto)
           THEN BLemma `pair-eta`
           THEN Auto))
   THEN D -1
   THEN HypSubst' (-2) 0
   THEN Auto)⋅ }

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

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
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])))
\mvdash{}  x  \mmember{}  a:A[p]  \mtimes{}  (b:B[p;a]  {}\mrightarrow{}  (\mcap{}n:\mBbbN{}.  (X  n  C[p;a;b])))


By

---

Latex:
((Assert  (x  \msim{}  <fst(x),  snd(x)>)  \mwedge{}  (fst(x)  \mmember{}  A[p])  BY
                (With  \mkleeneopen{}0\mkleeneclose{}  (D  (-1))\mcdot{}
                  THEN  Auto
                  THEN  (GenConcl  \mkleeneopen{}x  =  z\mkleeneclose{}\mcdot{}  THEN  Auto)
                  THEN  BLemma  `pair-eta`
                  THEN  Auto))
  THEN  D  -1
  THEN  HypSubst'  (-2)  0
  THEN  Auto)\mcdot{}

---

Home Index