{ [d1,d2:SecurityData].  (<d1, d2>  SecurityData) }

{ Proof }



Definitions occuring in Statement :  sdata-pair: <d1, d2>,  sdata: SecurityData,  uall: [x:A]. B[x],  member: t  T
Definitions :  uall: [x:A]. B[x],  sdata: SecurityData,  member: t  T,  sdata-pair: <d1, d2>
Lemmas :  node_wf,  tree_wf,  Id_wf

\mforall{}[d1,d2:SecurityData].    (<d1,  d2>  \mmember{}  SecurityData)


Date html generated: 2011_08_17-PM-07_07_11
Last ObjectModification: 2011_06_18-PM-12_50_46

Home Index