---

{ [pre:pi_prefix()]. [body:Pi_term].  (pre.body  Pi_term) }

{ Proof }

---

Definitions occuring in Statement :  picomm: pre.body,  pi_term: Pi_term,  pi_prefix: pi_prefix(),  uall: [x:A]. B[x],  member: t  T
Definitions :  uall: [x:A]. B[x],  pi_term: Pi_term,  member: t  T,  picomm: pre.body,  type-monotone: Monotone(T.F[T]),  uimplies: b supposing a
Lemmas :  name_wf,  unit_wf,  pi_prefix_wf,  subtype_rel_sum,  subtype_rel_simple_product

---

\mforall{}[pre:pi\_prefix()].  \mforall{}[body:Pi\_term].    (pre.body  \mmember{}  Pi\_term)


Date html generated: 2011_08_17-PM-06_41_46
Last ObjectModification: 2011_06_18-PM-12_08_51

Home Index