{ 
[val:Atom]. (val 
Expression) }
{ Proof }
Definitions occuring in Statement :
expbase: val,
expression: Expression,
uall: [x:A]. B[x],
member: t T,
atom: Atom
Definitions :
uall: [x:A]. B[x],
member: t T,
expression: Expression,
expbase: val,
type-monotone: Monotone(T.F[T]),
uimplies: b supposing a
Lemmas :
subtype_rel_sum,
subtype_rel_simple_product
\mforall{}[val:Atom]. (val \mmember{} Expression)
Date html generated:
2011_08_17-PM-04_33_20
Last ObjectModification:
2011_06_18-AM-11_44_07
Home
Index