Nuprl Lemma : ldst_wf

[l:IdLnk]. (destination(l) ∈ Id)


Proof




Definitions occuring in Statement :  ldst: destination(l) IdLnk: IdLnk Id: Id uall: [x:A]. B[x] member: t ∈ T
Lemmas :  Id_wf
\mforall{}[l:IdLnk].  (destination(l)  \mmember{}  Id)



Date html generated: 2015_07_17-AM-09_12_08
Last ObjectModification: 2015_01_28-AM-07_56_43

Home Index