---

Step * 1 of Lemma W-path-lemma


1. A : Type
2. B : A ⟶ Type
3. x : W(A;a.B[a])
4. alpha : ℕ ⟶ cw-step(A;a.B[a])
5. ∀n:ℕ. (W-rel(A;a.B[a];x) n alpha (alpha n))
⊢ alpha ∈ Path
BY
{ TACTIC:(MemTypeCD
          THEN Auto
          THEN (InstHyp [⌜i + 1⌝] (-2)⋅ THENA Auto)
          THEN MoveToConcl (-1)
          THEN RepUR ``param-W-rel W-rel`` 0
          THEN (Subst' (i + 1) - 1 ~ i 0 THENA Auto)
          THEN AutoSplit
          THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  x  :  W(A;a.B[a])
4.  alpha  :  \mBbbN{}  {}\mrightarrow{}  cw-step(A;a.B[a])
5.  \mforall{}n:\mBbbN{}.  (W-rel(A;a.B[a];x)  n  alpha  (alpha  n))
\mvdash{}  alpha  \mmember{}  Path


By

---

Latex:
TACTIC:(MemTypeCD
                THEN  Auto
                THEN  (InstHyp  [\mkleeneopen{}i  +  1\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
                THEN  MoveToConcl  (-1)
                THEN  RepUR  ``param-W-rel  W-rel``  0
                THEN  (Subst'  (i  +  1)  -  1  \msim{}  i  0  THENA  Auto)
                THEN  AutoSplit
                THEN  Auto)

---

Home Index