---

{ [A,A':Type].
    [B:A  Type]
      eq:EqDecider(A'). f,g:a:A fp-> B[a]. x:A'.
        [P,Q:a:A  B[a]  ].
          ((x:A. z:B[x].  (P[x;z]  Q[x;z]))
           z != f(x) ==> P[x;z]  z != g(x) ==> Q[x;z] supposing g  f) 
    supposing strong-subtype(A;A') }

{ Proof }

---

Definitions occuring in Statement :  fpf-sub: f  g,  fpf-val: z != f(x) ==> P[a; z],  fpf: a:A fp-> B[a],  uimplies: b supposing a,  uall: [x:A]. B[x],  prop: ,  so_apply: x[s1;s2],  so_apply: x[s],  all: x:A. B[x],  implies: P  Q,  function: x:A  B[x],  universe: Type,  deq: EqDecider(T),  strong-subtype: strong-subtype(A;B)
Definitions :  subtype: S  T,  member: t  T,  so_apply: x[s1;s2],  implies: P  Q,  all: x:A. B[x],  prop:
Lemmas :  deq-member_wf,  assert_wf

---

\mforall{}[A,A':Type].
    \mforall{}[B:A  {}\mrightarrow{}  Type]
        \mforall{}eq:EqDecider(A').  \mforall{}f,g:a:A  fp->  B[a].  \mforall{}x:A'.
            \mforall{}[P,Q:a:A  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbP{}].
                ((\mforall{}x:A.  \mforall{}z:B[x].    (P[x;z]  {}\mRightarrow{}  Q[x;z]))
                {}\mRightarrow{}  z  !=  f(x)  ==>  P[x;z]  {}\mRightarrow{}  z  !=  g(x)  ==>  Q[x;z]  supposing  g  \msubseteq{}  f) 
    supposing  strong-subtype(A;A')


Date html generated: 2011_08_10-AM-08_02_19
Last ObjectModification: 2011_06_18-AM-08_20_22

Home Index