---

{ [A:Type]. [B1:Void  Type]. [B2:A  Type].
    (a:Void fp-> B1[a] r a:A fp-> B2[a]) }

{ Proof }

---

Definitions occuring in Statement :  fpf: a:A fp-> B[a],  subtype_rel: A r B,  uall: [x:A]. B[x],  so_apply: x[s],  function: x:A  B[x],  void: Void,  universe: Type
Definitions :  uall: [x:A]. B[x],  fpf: a:A fp-> B[a],  so_apply: x[s],  member: t  T,  all: x:A. B[x],  subtype: S  T,  suptype: suptype(S; T),  so_lambda: x.t[x],  implies: P  Q,  false: False,  iff: P  Q,  and: P  Q,  prop:
Lemmas :  nil_member,  l_member_wf,  fpf_wf

---

\mforall{}[A:Type].  \mforall{}[B1:Void  {}\mrightarrow{}  Type].  \mforall{}[B2:A  {}\mrightarrow{}  Type].    (a:Void  fp->  B1[a]  \msubseteq{}r  a:A  fp->  B2[a])


Date html generated: 2011_08_10-AM-07_54_40
Last ObjectModification: 2011_06_18-AM-08_15_08

Home Index