---

{ [ds,ds':ltg:Id fp-> Type].  State(ds')  State(ds) supposing ds  ds' }

{ Proof }

---

Definitions occuring in Statement :  ma-state: State(ds),  fpf-sub: f  g,  fpf: a:A fp-> B[a],  id-deq: IdDeq,  Id: Id,  uimplies: b supposing a,  uall: [x:A]. B[x],  subtype: S  T,  universe: Type
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  subtype: S  T,  member: t  T,  all: x:A. B[x],  so_lambda: x.t[x],  so_apply: x[s],  prop:
Lemmas :  ma-state-subtype,  ma-state_wf,  fpf-sub_wf,  Id_wf,  id-deq_wf,  fpf_wf

---

\mforall{}[ds,ds':ltg:Id  fp->  Type].    State(ds')  \msubseteq{}  State(ds)  supposing  ds  \msubseteq{}  ds'


Date html generated: 2011_08_10-AM-08_12_20
Last ObjectModification: 2011_06_18-AM-08_27_25

Home Index