{ 
[left,right:Pi_term]. ((left + right) 
Pi_term) }
{ Proof }
Definitions occuring in Statement :
pioption: (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,
pioption: (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_41_54
Last ObjectModification:
2011_06_18-PM-12_09_06
Home
Index