{ 
[body:Pi_term]. (!body 
Pi_term) }
{ Proof }
Definitions occuring in Statement :
pirep: !body,
pi_term: Pi_term,
uall: [x:A]. B[x],
member: t T
Definitions :
uall: [x:A]. B[x],
pi_term: Pi_term,
member: t T,
pirep: !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{}[body:Pi\_term]. (!body \mmember{} Pi\_term)
Date html generated:
2011_08_17-PM-06_42_11
Last ObjectModification:
2011_06_18-PM-12_09_37
Home
Index