---

Step * 3 of Lemma W-path-lemma2


1. A1 : Type
2. B1 : A1 ⟶ Type
3. pco-W ⋅ ≡ a:A1 × (b:(B1 a) ⟶ (pco-W ⋅))
4. a : A1
5. x1 : B1[a] ⟶ W(A1;a.B1[a])
6. n : ℕ+
7. s : ℕn ⟶ cw-step(A1;a.B1[a])
8. a1 : A1
9. w1 : b:B1[a1] ⟶ (pco-W ⋅)
10. x : B1[a1]
11. a2 : A1
12. z1 : b:B1[a2] ⟶ (pco-W ⋅)
13. k : ℕn
⊢ <a, x1> ∈ W(A1;a.B1[a])
BY
{ (DWtype 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A1  :  Type
2.  B1  :  A1  {}\mrightarrow{}  Type
3.  pco-W  \mcdot{}  \mequiv{}  a:A1  \mtimes{}  (b:(B1  a)  {}\mrightarrow{}  (pco-W  \mcdot{}))
4.  a  :  A1
5.  x1  :  B1[a]  {}\mrightarrow{}  W(A1;a.B1[a])
6.  n  :  \mBbbN{}\msupplus{}
7.  s  :  \mBbbN{}n  {}\mrightarrow{}  cw-step(A1;a.B1[a])
8.  a1  :  A1
9.  w1  :  b:B1[a1]  {}\mrightarrow{}  (pco-W  \mcdot{})
10.  x  :  B1[a1]
11.  a2  :  A1
12.  z1  :  b:B1[a2]  {}\mrightarrow{}  (pco-W  \mcdot{})
13.  k  :  \mBbbN{}n
\mvdash{}  <a,  x1>  \mmember{}  W(A1;a.B1[a])


By

---

Latex:
(DWtype  0  THEN  Auto)

---

Home Index