Nuprl Lemma : lnk-inv-one-one

[l1,l2:IdLnk].  uiff(lnk-inv(l1) lnk-inv(l2) ∈ IdLnk;l1 l2 ∈ IdLnk)


Proof




Definitions occuring in Statement :  lnk-inv: lnk-inv(l) IdLnk: IdLnk uiff: uiff(P;Q) uall: [x:A]. B[x] equal: t ∈ T
Lemmas :  equal_wf IdLnk_wf lnk-inv_wf and_wf lnk-inv-inv iff_weakening_equal
\mforall{}[l1,l2:IdLnk].    uiff(lnk-inv(l1)  =  lnk-inv(l2);l1  =  l2)



Date html generated: 2015_07_17-AM-09_10_56
Last ObjectModification: 2015_02_04-PM-05_07_50

Home Index