{ 
[name:Name]. [body:Pi_term]. ((new name. body) 
Pi_term) }
{ Proof }
Definitions occuring in Statement :
pinew: (new name. body),
pi_term: Pi_term,
name: Name,
uall: [x:A]. B[x],
member: t T
Definitions :
uall: [x:A]. B[x],
pi_term: Pi_term,
member: t T,
pinew: (new name. body),
type-monotone: Monotone(T.F[T]),
uimplies: b supposing a
Lemmas :
pi_prefix_wf,
unit_wf,
name_wf,
subtype_rel_sum,
subtype_rel_simple_product
\mforall{}[name:Name]. \mforall{}[body:Pi\_term]. ((new name. body) \mmember{} Pi\_term)
Date html generated:
2011_08_17-PM-06_42_20
Last ObjectModification:
2011_06_18-PM-12_09_52
Home
Index