for @{ 'explicitset (\lambda ${ident x} : $t . $p) }.
definition mk_set ≝ λT:bishop_set.λx:T→Prop.x.
interpretation "explicit set" 'explicitset t = (mk_set _ t).
for @{ 'explicitset (\lambda ${ident x} : $t . $p) }.
definition mk_set ≝ λT:bishop_set.λx:T→Prop.x.
interpretation "explicit set" 'explicitset t = (mk_set _ t).