Nuprl Definition : vr_parmEXT
vr_parmEXT(G;A;B) == 
a1,a2:A. b1,b2:B. ((a1 = a2) 
(b1 = b2) (G a1 b1 
G a2 b2))
Definitions occuring in Statement :
all: x:A. B[x],
iff: P Q,
implies: P Q,
apply: f a,
equal: s = t
FDL editor aliases :
vr_parmEXT
vr\_parmEXT(G;A;B) == \mforall{}a1,a2:A. \mforall{}b1,b2:B. ((a1 = a2) {}\mRightarrow{} (b1 = b2) {}\mRightarrow{} (G a1 b1 \mLeftarrow{}{}\mRightarrow{} G a2 b2))
Date html generated:
2012_02_20-PM-03_33_05
Last ObjectModification:
2012_02_02-PM-01_55_16
Home
Index