---

Step * 2 of Lemma W-path-lemma2

.....wf..... 
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. (W-rel(A1;a.B1[a];<a, x1>) k s (s k))
⊢ <⋅, <a1, w1>, inl x> ∈ cw-step(A1;a.B1[a])
BY
{ (RepUR ``cw-step pcw-step`` 0 THEN Auto THEN Try ((pcoWD (-1) THEN Auto))) }

1
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. (W-rel(A1;a.B1[a];<a, x1>) k s (s k))
⊢ <a1, w1> ∈ pco-W ⋅

---

Latex:

---

Latex:
.....wf..... 
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.  \mforall{}k:\mBbbN{}n.  (W-rel(A1;a.B1[a];<a,  x1>)  k  s  (s  k))
\mvdash{}  <\mcdot{},  <a1,  w1>,  inl  x>  \mmember{}  cw-step(A1;a.B1[a])


By

---

Latex:
(RepUR  ``cw-step  pcw-step``  0  THEN  Auto  THEN  Try  ((pcoWD  (-1)  THEN  Auto)))

---

Home Index