{ 
[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