---

{ [M:Type  Type]
    [A,B:Type].  (Com(P.M[P]) A) r (Com(P.M[P]) B) supposing A r B 
    supposing A,B:Type.  ((A r B)  (M[A] r M[B])) }

{ Proof }

---

Definitions occuring in Statement :  Com: Com(P.M[P]),  subtype_rel: A r B,  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s],  all: x:A. B[x],  implies: P  Q,  apply: f a,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  all: x:A. B[x],  implies: P  Q,  so_apply: x[s],  Com: Com(P.M[P]),  member: t  T,  tag-case: z:T,  ifthenelse: if b then t else f fi ,  so_lambda: x.t[x],  btrue: tt,  prop: ,  bfalse: ff,  bool: ,  unit: Unit,  iff: P  Q,  and: P  Q,  it: ,  guard: {T}
Lemmas :  tagged+_wf,  tag-case_wf,  Id_wf,  unit_wf,  subtype_rel_tagged+,  subtype_rel_self,  subtype_rel_product,  ifthenelse_wf,  eq_atom_wf,  bool_wf,  iff_weakening_uiff,  uiff_transitivity,  assert_wf,  eqtt_to_assert,  assert_of_eq_atom,  not_wf,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  not_functionality_wrt_uiff

---

\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[A,B:Type].    (Com(P.M[P])  A)  \msubseteq{}r  (Com(P.M[P])  B)  supposing  A  \msubseteq{}r  B 
    supposing  \mforall{}A,B:Type.    ((A  \msubseteq{}r  B)  {}\mRightarrow{}  (M[A]  \msubseteq{}r  M[B]))


Date html generated: 2011_08_16-PM-06_47_20
Last ObjectModification: 2011_06_18-AM-10_59_33

Home Index