---

Step * of Lemma W-path-lemma

∀A:Type. ∀B:A ⟶ Type. ∀x:W(A;a.B[a]). ∀alpha:ℕ ⟶ cw-step(A;a.B[a]).
  ((∀n:ℕ. (W-rel(A;a.B[a];x) n alpha (alpha n))) ⇒ (alpha ∈ Path))
BY
{ TACTIC:Auto }

1
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

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}B:A  {}\mrightarrow{}  Type.  \mforall{}x:W(A;a.B[a]).  \mforall{}alpha:\mBbbN{}  {}\mrightarrow{}  cw-step(A;a.B[a]).
    ((\mforall{}n:\mBbbN{}.  (W-rel(A;a.B[a];x)  n  alpha  (alpha  n)))  {}\mRightarrow{}  (alpha  \mmember{}  Path))


By

---

Latex:
TACTIC:Auto

---

Home Index