---

{ [fun:Atom]. [arg:Expression].  (fun(arg)  Expression) }

{ Proof }

---

Definitions occuring in Statement :  expapply: fun(arg),  expression: Expression,  uall: [x:A]. B[x],  member: t  T,  atom: Atom
Definitions :  uall: [x:A]. B[x],  expression: Expression,  member: t  T,  expapply: fun(arg),  type-monotone: Monotone(T.F[T]),  uimplies: b supposing a
Lemmas :  subtype_rel_sum,  subtype_rel_simple_product

---

\mforall{}[fun:Atom].  \mforall{}[arg:Expression].    (fun(arg)  \mmember{}  Expression)


Date html generated: 2011_08_17-PM-04_33_36
Last ObjectModification: 2011_06_18-AM-11_44_32

Home Index