---

Step * 1 of Lemma es-causle-retraction-squash


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)
BY
{ (InstLemma `es-causl-swellfnd` [⌈es⌉]⋅ THENA 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
6. SWellFounded((e < e'))
⊢ retraction(T;f)

---

Latex:



1.  es  :  EO@i'
2.  [T]  :  Type
3.  strong-subtype(T;E)
4.  f  :  T  {}\mrightarrow{}  T@i
5.  \mforall{}x:T.  f  x  c\mleq{}  x@i
\mvdash{}  retraction(T;f)


By

(InstLemma  `es-causl-swellfnd`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index