---

Step * of Lemma W-path-lemma2

∀A1:Type. ∀B1:A1 ⟶ Type. ∀a:A1. ∀x1:B1[a] ⟶ W(A1;a.B1[a]). ∀n:ℕ+. ∀s:ℕn ⟶ cw-step(A1;a.B1[a]). ∀a1:A1.
∀w1:b:B1[a1] ⟶ (pco-W ⋅). ∀x:B1[a1]. ∀a2:A1. ∀z1:b:B1[a2] ⟶ (pco-W ⋅).
  ((∀k:ℕn. (W-rel(A1;a.B1[a];<a, x1>) k s (s k)))
  ⇒ ((s (n - 1)) = <⋅, <a1, w1>, inl x> ∈ cw-step(A1;a.B1[a]))
  ⇒ ((w1 x) = <a2, z1> ∈ (pco-W ⋅))
  ⇒ (z1 ∈ b:B1[a2] ⟶ W(A1;a.B1[a])))
BY
{ (RepeatFor 2 (Intro)
   THEN (InstLemma `param-co-W-ext` [⌜Unit⌝;⌜λ2p.A1⌝;⌜λ2p a.B1 a⌝;⌜so_lambda(p,a,b.⋅)⌝]⋅ THENA Auto)
   THEN (D -1 With ⌜⋅⌝  THENA Auto)
   THEN Reduce -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))
14. (s (n - 1)) = <⋅, <a1, w1>, inl x> ∈ cw-step(A1;a.B1[a])
15. (w1 x) = <a2, z1> ∈ (pco-W ⋅)
⊢ z1 ∈ b:B1[a2] ⟶ W(A1;a.B1[a])

2
.....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])

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

---

Latex:

---

Latex:
\mforall{}A1:Type.  \mforall{}B1:A1  {}\mrightarrow{}  Type.  \mforall{}a:A1.  \mforall{}x1:B1[a]  {}\mrightarrow{}  W(A1;a.B1[a]).  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  cw-step(A1;a.B1[a]).
\mforall{}a1:A1.  \mforall{}w1:b:B1[a1]  {}\mrightarrow{}  (pco-W  \mcdot{}).  \mforall{}x:B1[a1].  \mforall{}a2:A1.  \mforall{}z1:b:B1[a2]  {}\mrightarrow{}  (pco-W  \mcdot{}).
    ((\mforall{}k:\mBbbN{}n.  (W-rel(A1;a.B1[a];<a,  x1>)  k  s  (s  k)))
    {}\mRightarrow{}  ((s  (n  -  1))  =  <\mcdot{},  <a1,  w1>,  inl  x>)
    {}\mRightarrow{}  ((w1  x)  =  <a2,  z1>)
    {}\mRightarrow{}  (z1  \mmember{}  b:B1[a2]  {}\mrightarrow{}  W(A1;a.B1[a])))


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  (InstLemma  `param-co-W-ext`  [\mkleeneopen{}Unit\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p.A1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p  a.B1  a\mkleeneclose{};\mkleeneopen{}so\_lambda(p,a,b.\mcdot{})\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}\mcdot{}\mkleeneclose{}    THENA  Auto)
  THEN  Reduce  -1
  THEN  Auto)

---

Home Index