---

Step * 1 1 1 1 of Lemma Spread-family-ext


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
10. a : P
11. b : Mv[f (fst(x));p;a]
12. n : ℕ
⊢ (snd(x)) a b ∈ X n a
BY
{ (With ⌜n⌝ (DVar `x')⋅ THEN Auto THEN (GenConcl ⌜x = z ∈ (a:Pos × (q:P ⟶ Mv[f a;p;q] ⟶ (X n q)))⌝⋅ THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:

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)))
8.  x  \msim{}  <fst(x),  snd(x)>
9.  fst(x)  \mmember{}  Pos
10.  a  :  P
11.  b  :  Mv[f  (fst(x));p;a]
12.  n  :  \mBbbN{}
\mvdash{}  (snd(x))  a  b  \mmember{}  X  n  a


By

---

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

---

Home Index