---

Step * 1 of Lemma fun-path-cons


1. T : Type
2. f : T ⟶ T
3. x : T
4. y : T
5. z : T
⊢ uiff(z=f*(x) via [y];{(z = y ∈ T)
∧ ((y = (f hd([])) ∈ T) ∧ (¬(y = hd([]) ∈ T))) ∧ hd([])=f*(x) via [] supposing 0 < ||[]||
∧ x = y ∈ T supposing ¬0 < ||[]||})
BY
{ (RepUR ``guard fun-path last`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  x  :  T
4.  y  :  T
5.  z  :  T
\mvdash{}  uiff(z=f*(x)  via  [y];\{(z  =  y)
\mwedge{}  ((y  =  (f  hd([])))  \mwedge{}  (\mneg{}(y  =  hd([]))))  \mwedge{}  hd([])=f*(x)  via  []  supposing  0  <  ||[]||
\mwedge{}  x  =  y  supposing  \mneg{}0  <  ||[]||\})


By

---

Latex:
(RepUR  ``guard  fun-path  last``  0  THEN  Auto)

---

Home Index