for @{ 'subset $a $u }.
interpretation "Bishop subset" 'subset a b = (subset _ a b).
-notation "hvbox({ ident x : t | break p })" non associative with precedence 50
+notation "hvbox({ ident x : t | break p })" non associative with precedence 80
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).