e<e'.P[e] == e:E. ((e <loc e') 
P[e])
Definitions :
all: x:A. B[x],
es-E: E,
implies: P Q,
es-locl: (e <loc e')
FDL editor aliases :
alle-lt
\mforall{}e<e'.P[e] == \mforall{}e:E. ((e <loc e') {}\mRightarrow{} P[e])
Date html generated:
2010_08_27-AM-09_28_01
Last ObjectModification:
2009_12_16-AM-01_02_34
Home
Index