---

{ [A1,A2,A3:Type]. [d,d':EqDecider(A3)]. [d2:EqDecider(A2)].
  [f:a:A1 fp-> Type]. [g:a:A2 fp-> Type]. [x:A3].
    ({g(x)?Top r f(x)?Top supposing f  g}) supposing 
       (strong-subtype(A2;A3) and 
       strong-subtype(A1;A2)) }

{ Proof }

---

Definitions occuring in Statement :  fpf-sub: f  g,  fpf-cap: f(x)?z,  fpf: a:A fp-> B[a],  subtype_rel: A r B,  uimplies: b supposing a,  uall: [x:A]. B[x],  top: Top,  guard: {T},  universe: Type,  deq: EqDecider(T),  strong-subtype: strong-subtype(A;B)
Definitions :  so_lambda: x.t[x],  all: x:A. B[x],  member: t  T,  so_apply: x[s],  implies: P  Q,  cand: A c B,  strong-subtype: strong-subtype(A;B),  false: False,  not: A
Lemmas :  subtype_rel_self,  subtype-fpf3

---

\mforall{}[A1,A2,A3:Type].  \mforall{}[d,d':EqDecider(A3)].  \mforall{}[d2:EqDecider(A2)].  \mforall{}[f:a:A1  fp->  Type].
\mforall{}[g:a:A2  fp->  Type].  \mforall{}[x:A3].
    (\{g(x)?Top  \msubseteq{}r  f(x)?Top  supposing  f  \msubseteq{}  g\})  supposing 
          (strong-subtype(A2;A3)  and 
          strong-subtype(A1;A2))


Date html generated: 2011_08_10-AM-07_58_07
Last ObjectModification: 2011_06_18-AM-08_18_08

Home Index