---

Step * of Lemma fix-step

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[f:T ⟶ T]. ∀[x:T].  f**(f x) = f**(x) ∈ T supposing retraction(T;f)
BY
{ Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. f : T ⟶ T
4. x : T
5. retraction(T;f)
⊢ f**(f x) = f**(x) ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[f:T  {}\mrightarrow{}  T].  \mforall{}[x:T].    f**(f  x)  =  f**(x)  supposing  retraction(T;f)


By

---

Latex:
Auto

---

Home Index