Nuprl Lemma : eo-forward-equal-info-body
∀[f,es,T,e,e',v:Top]. (v = body(e) ~ v = body(e))
Proof
Definitions occuring in Statement :
equal-info-body: v = body(e),
eo-forward: eo.e,
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Lemmas :
top_wf,
eo-forward-info
Latex:
\mforall{}[f,es,T,e,e',v:Top]. (v = body(e) \msim{} v = body(e))
Date html generated:
2015_07_21-PM-04_48_55
Last ObjectModification:
2015_01_28-AM-08_45_51
Home
Index