Nuprl Lemma : eo-strict-forward-loc

[eo,e,e':Top].  (loc(e') loc(e'))


Proof




Definitions occuring in Statement :  eo-strict-forward: eo>e es-loc: loc(e) uall: [x:A]. B[x] top: Top sqequal: t
Lemmas :  rec_select_update_lemma top_wf
\mforall{}[eo,e,e':Top].    (loc(e')  \msim{}  loc(e'))



Date html generated: 2015_07_17-PM-00_07_00
Last ObjectModification: 2015_01_28-AM-00_11_16

Home Index