---

Step * 1 of Lemma fun-path-fixedpoint


1. T : Type
2. f : T ⟶ T
⊢ ∀[x,y,z:T].  (y = z ∈ T) supposing (((f y) = y ∈ T) and (y ∈ []) and z=f*(x) via [])
BY
{ (RepUR ``fun-path`` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
\mvdash{}  \mforall{}[x,y,z:T].    (y  =  z)  supposing  (((f  y)  =  y)  and  (y  \mmember{}  [])  and  z=f*(x)  via  [])


By

---

Latex:
(RepUR  ``fun-path``  0  THEN  Auto)\mcdot{}

---

Home Index