{ 
[left,right:Pi_term]. ((left | right) 
Pi_term) }
{ Proof }
Definitions occuring in Statement :
pipar: (left | right),
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,
pipar: (left | right),
type-monotone: Monotone(T.F[T]),
uimplies: b supposing a
Lemmas :
name_wf,
pi_prefix_wf,
unit_wf,
subtype_rel_sum,
subtype_rel_simple_product
\mforall{}[left,right:Pi\_term]. ((left | right) \mmember{} Pi\_term)
Date html generated:
2011_08_17-PM-06_42_03
Last ObjectModification:
2011_06_18-PM-12_09_22
Home
Index