---

Step * of Lemma es-causle-retraction-squash

∀es:EO. ∀[T:Type]. ∀f:T ─→ T. ((∀x:T. f x c≤ x) ⇒ retraction(T;f)) supposing strong-subtype(T;E)
BY
{ (Auto THEN Try ((DoSubsume THEN Auto))) }

1
1. es : EO@i'
2. [T] : Type
3. strong-subtype(T;E)
4. f : T ─→ T@i
5. ∀x:T. f x c≤ x@i
⊢ retraction(T;f)

---

Latex:


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


By

(Auto  THEN  Try  ((DoSubsume  THEN  Auto)))

---

Home Index