---

Step * of Lemma fix_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[f:T ⟶ T].  ∀[x:T]. (f**(x) ∈ T) supposing retraction(T;f)
BY
{ (Auto THEN MoveToConcl (-1) THEN D -1) }

1
1. T : Type
2. eq : EqDecider(T)
3. f : T ⟶ T
4. h : T ⟶ ℕ
5. ∀x:T. (((f x) = x ∈ T) ∨ h (f x) < h x)
⊢ ∀x:T. (f**(x) ∈ T)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  MoveToConcl  (-1)  THEN  D  -1)

---

Home Index