{ link 1 from a to b  IdLnk }

{ Proof }



Definitions occuring in Statement :  mklnk: link $n from $a to $b,  IdLnk: IdLnk,  member: t  T
Definitions :  member: t  T,  IdLnk: IdLnk,  mklnk: link $n from $a to $b,  Id: Id,  mkid: "$x"
Lemmas :  IdLnk_wf,  member_wf,  Id_wf

link  1  from  a  to  b  \mmember{}  IdLnk


Date html generated: 2011_08_10-AM-07_43_32
Last ObjectModification: 2011_06_18-AM-08_10_02

Home Index