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