---

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

{ Proof }

---

Definitions occuring in Statement :  es-fix: f**(e),  es-eq-E: e = e',  ifthenelse: if b then t else f fi ,  uall: [x:A]. B[x],  top: Top,  apply: f a,  sqequal: s ~ t
Definitions :  uall: [x:A]. B[x],  es-fix: f**(e),  es-eq-E: e = e',  member: t  T,  fix: f**(x),  ycomb: Y
Lemmas :  top_wf

---

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


Date html generated: 2011_08_16-AM-10_32_31
Last ObjectModification: 2011_06_18-AM-09_14_08

Home Index