---

{ [s:SES]. (Info  Type) }

{ Proof }

---

Definitions occuring in Statement :  ses-info: Info,  security-event-structure: SES,  uall: [x:A]. B[x],  member: t  T,  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  ses-info: Info,  top: Top,  security-event-structure: SES
Lemmas :  pi1_wf_top,  security-event-structure_wf

---

\mforall{}[s:SES].  (Info  \mmember{}  Type)


Date html generated: 2011_08_17-PM-07_11_42
Last ObjectModification: 2011_06_18-PM-12_57_34

Home Index