---

Step * of Lemma es-fix-cases

∀[es,f,e:Top].  (f**(e) ~ if e = f e then e else f**(f e) fi )
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `es-fix` 0
   THEN RW (AddrC [1] (RecUnfoldC `fix`)) 0
   THEN RepUR ``es-eq-E eqof`` 0
   THEN Auto) }

---

Latex:


\mforall{}[es,f,e:Top].    (f**(e)  \msim{}  if  e  =  f  e  then  e  else  f**(f  e)  fi  )


By

((UnivCD  THENA  Auto)
  THEN  Unfold  `es-fix`  0
  THEN  RW  (AddrC  [1]  (RecUnfoldC  `fix`))  0
  THEN  RepUR  ``es-eq-E  eqof``  0
  THEN  Auto)

---

Home Index