:: HIDDEN semantic presentation
definition
mode
set
->
set
;
end;
definition
let
c
1
,
c
2
be
set
;
pred
c
1
=
c
2
;
reflexivity
errorfrm
;
symmetry
errorfrm
;
end;
notation
end;
definition
let
c
1
,
c
2
be
set
;
pred
c
1
in
c
2
;
asymmetry
errorfrm
;
end;