---

{ [a:Atom1]. (data(a)  SecurityData) }

{ Proof }

---

Definitions occuring in Statement :  atom-sdata: data(a),  sdata: SecurityData,  uall: [x:A]. B[x],  member: t  T,  atom: Atom$n
Definitions :  uall: [x:A]. B[x],  member: t  T,  sdata: SecurityData,  atom-sdata: data(a)
Lemmas :  tree_leaf_wf2,  Id_wf

---

\mforall{}[a:Atom1].  (data(a)  \mmember{}  SecurityData)


Date html generated: 2011_08_17-PM-07_07_02
Last ObjectModification: 2011_06_18-PM-12_50_29

Home Index