{ [x:Id]. (data(x)  SecurityData) }

{ Proof }



Definitions occuring in Statement :  id-sdata: data(x),  sdata: SecurityData,  Id: Id,  uall: [x:A]. B[x],  member: t  T
Definitions :  uall: [x:A]. B[x],  member: t  T,  sdata: SecurityData,  id-sdata: data(x)
Lemmas :  tree_leaf_wf2,  Id_wf

\mforall{}[x:Id].  (data(x)  \mmember{}  SecurityData)


Date html generated: 2011_08_17-PM-07_06_53
Last ObjectModification: 2011_06_18-PM-12_50_13

Home Index