Nuprl Definition : vr_EXT
vr_EXT == 
[T:Type]. [A,B:T 
]. (A ~~ B 
(A = B))
Definitions occuring in Statement :
vr_equi-pred: X ~~ Y,
uall: [x:A]. B[x],
prop: ,
implies: P Q,
function: x:A B[x],
universe: Type,
equal: s = t
FDL editor aliases :
vr_EXT
vr\_EXT == \mforall{}[T:Type]. \mforall{}[A,B:T {}\mrightarrow{} \mBbbP{}]. (A \msim{}\msim{} B {}\mRightarrow{} (A = B))
Date html generated:
2012_02_20-PM-03_33_45
Last ObjectModification:
2012_02_02-PM-01_55_25
Home
Index