Nuprl Lemma : islocal-implies
∀[k:Knd]. locl(act(k)) = k ∈ Knd supposing ↑islocal(k)
Proof
Definitions occuring in Statement :
actof: act(k),
locl: locl(a),
islocal: islocal(k),
Knd: Knd,
assert: ↑b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Lemmas :
false_wf,
locl_wf,
true_wf,
assert_wf,
islocal_wf,
Knd_wf
\mforall{}[k:Knd]. locl(act(k)) = k supposing \muparrow{}islocal(k)
Date html generated:
2015_07_17-AM-09_11_50
Last ObjectModification:
2015_01_28-AM-07_56_55
Home
Index