---

Step * 1 1 of Lemma Spread-family-ext

.....subterm..... T:t
1:n
1. P : Type
2. Pos : Type
3. f : Pos ⟶ ℤ
4. Mv : ℤ ⟶ P ⟶ P ⟶ Type
5. X : ℕ ⟶ P ⟶ Type
6. p : P
7. x : ⋂n:ℕ. (a:Pos × (q:P ⟶ Mv[f a;p;q] ⟶ (X n q)))
⊢ x ∈ a:Pos × (q:P ⟶ Mv[f a;p;q] ⟶ (⋂n:ℕ. (X n q)))
BY
{ ((Assert (x ~ <fst(x), snd(x)>) ∧ (fst(x) ∈ Pos) BY
          (With ⌜0⌝ (D (-1))⋅
           THEN Auto
           THEN (GenConcl ⌜x = z ∈ (a:Pos × (q:P ⟶ Mv[f a;p;q] ⟶ (X 0 q)))⌝⋅ THEN Auto)
           THEN BLemma `pair-eta`
           THEN Auto))
   THEN D -1
   THEN HypSubst' (-2) 0
   THEN Auto) }

1
1. P : Type
2. Pos : Type
3. f : Pos ⟶ ℤ
4. Mv : ℤ ⟶ P ⟶ P ⟶ Type
5. X : ℕ ⟶ P ⟶ Type
6. p : P
7. x : ⋂n:ℕ. (a:Pos × (q:P ⟶ Mv[f a;p;q] ⟶ (X n q)))
8. x ~ <fst(x), snd(x)>
9. fst(x) ∈ Pos
⊢ snd(x) ∈ q:P ⟶ Mv[f (fst(x));p;q] ⟶ (⋂n:ℕ. (X n q))

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  P  :  Type
2.  Pos  :  Type
3.  f  :  Pos  {}\mrightarrow{}  \mBbbZ{}
4.  Mv  :  \mBbbZ{}  {}\mrightarrow{}  P  {}\mrightarrow{}  P  {}\mrightarrow{}  Type
5.  X  :  \mBbbN{}  {}\mrightarrow{}  P  {}\mrightarrow{}  Type
6.  p  :  P
7.  x  :  \mcap{}n:\mBbbN{}.  (a:Pos  \mtimes{}  (q:P  {}\mrightarrow{}  Mv[f  a;p;q]  {}\mrightarrow{}  (X  n  q)))
\mvdash{}  x  \mmember{}  a:Pos  \mtimes{}  (q:P  {}\mrightarrow{}  Mv[f  a;p;q]  {}\mrightarrow{}  (\mcap{}n:\mBbbN{}.  (X  n  q)))


By

---

Latex:
((Assert  (x  \msim{}  <fst(x),  snd(x)>)  \mwedge{}  (fst(x)  \mmember{}  Pos)  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)

---

Home Index