Nuprl Lemma : concat-lifting-loc-1-strict
∀[f,i:Top]. (f@ i {} ~ {})
Proof
Definitions occuring in Statement :
concat-lifting-loc-1: f@,
uall: ∀[x:A]. B[x],
top: Top,
apply: f a,
sqequal: s ~ t,
empty-bag: {}
Lemmas :
top_wf,
has-value_wf_base,
lifting-strict-int_eq,
base_wf
Latex:
\mforall{}[f,i:Top]. (f@ i \{\} \msim{} \{\})
Date html generated:
2015_07_22-PM-00_08_12
Last ObjectModification:
2015_01_28-AM-11_41_56
Home
Index