---

Step * of Lemma es-fix_wf

∀[es:EO]. ∀[T:Type].  ∀[f:T ⟶ T]. ∀[e:T]. (f**(e) ∈ T) supposing ∀x:T. f x c≤ x supposing strong-subtype(T;E)
BY
{ (Auto THEN Unfold `es-fix` 0) }

1
1. es : EO
2. T : Type
3. strong-subtype(T;E)
4. f : T ⟶ T
5. ∀x:T. f x c≤ x
6. e : T
⊢ f**(e) ∈ T

---

Latex:

---

Latex:
\mforall{}[es:EO].  \mforall{}[T:Type].
    \mforall{}[f:T  {}\mrightarrow{}  T].  \mforall{}[e:T].  (f**(e)  \mmember{}  T)  supposing  \mforall{}x:T.  f  x  c\mleq{}  x  supposing  strong-subtype(T;E)


By

---

Latex:
(Auto  THEN  Unfold  `es-fix`  0)

---

Home Index