Nuprl Lemma : lsrc-inv

[l:IdLnk]. (source(lnk-inv(l)) destination(l))


Proof




Definitions occuring in Statement :  ldst: destination(l) lsrc: source(l) lnk-inv: lnk-inv(l) IdLnk: IdLnk uall: [x:A]. B[x] sqequal: t
Lemmas :  Id_wf
\mforall{}[l:IdLnk].  (source(lnk-inv(l))  \msim{}  destination(l))



Date html generated: 2015_07_17-AM-09_12_28
Last ObjectModification: 2015_01_28-AM-07_56_22

Home Index