---

{ [A,A':Type].
    [B:A  Type]. [C:A'  Type]. [eq:EqDecider(A)]. [eq':EqDecider(A')].
    [f,g:a:A fp-> B[a]].
      {f  g supposing f  g} supposing a:A. (B[a] r C[a]) 
    supposing strong-subtype(A;A') }

{ Proof }

---

Definitions occuring in Statement :  fpf-sub: f  g,  fpf: a:A fp-> B[a],  subtype_rel: A r B,  uimplies: b supposing a,  uall: [x:A]. B[x],  guard: {T},  so_apply: x[s],  all: x:A. B[x],  function: x:A  B[x],  universe: Type,  deq: EqDecider(T),  strong-subtype: strong-subtype(A;B)
Definitions :  guard: {T}
Lemmas :  fpf-sub-functionality

---

\mforall{}[A,A':Type].
    \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[C:A'  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[eq':EqDecider(A')].  \mforall{}[f,g:a:A  fp->  B[a]].
        \{f  \msubseteq{}  g  supposing  f  \msubseteq{}  g\}  supposing  \mforall{}a:A.  (B[a]  \msubseteq{}r  C[a]) 
    supposing  strong-subtype(A;A')


Date html generated: 2011_08_10-AM-07_57_15
Last ObjectModification: 2011_06_18-AM-08_17_34

Home Index