---

{ [A1,A2:Type]. [B1:A1  Type]. [B2:A2  Type].
    (a:A1 fp-> B1[a] r a:A2 fp-> B2[a]) supposing 
       ((a:A1. (B1[a] r B2[a])) and 
       strong-subtype(A1;A2)) }

{ Proof }

---

Definitions occuring in Statement :  fpf: a:A fp-> B[a],  subtype_rel: A r B,  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s],  all: x:A. B[x],  function: x:A  B[x],  universe: Type,  strong-subtype: strong-subtype(A;B)
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  strong-subtype: strong-subtype(A;B),  all: x:A. B[x],  so_apply: x[s],  cand: A c B,  exists: x:A. B[x],  implies: P  Q,  member: t  T,  so_lambda: x.t[x],  prop: ,  fpf: a:A fp-> B[a],  subtype: S  T,  l_member: (x  l),  le: A  B,  not: A,  false: False,  nat: ,  length: ||as||,  select: l[i],  ycomb: Y,  or: P  Q,  iff: P  Q,  and: P  Q,  guard: {T}
Lemmas :  fpf_wf,  l_member_wf,  cons_member,  length_wf1,  select_wf,  nat_properties

---

\mforall{}[A1,A2:Type].  \mforall{}[B1:A1  {}\mrightarrow{}  Type].  \mforall{}[B2:A2  {}\mrightarrow{}  Type].
    (a:A1  fp->  B1[a]  \msubseteq{}r  a:A2  fp->  B2[a])  supposing 
          ((\mforall{}a:A1.  (B1[a]  \msubseteq{}r  B2[a]))  and 
          strong-subtype(A1;A2))


Date html generated: 2011_08_10-AM-07_54_38
Last ObjectModification: 2011_06_18-AM-08_15_06

Home Index