notation "hvbox(x break ∉ A)" with precedence 60
for @{ 'not_member_of $x $A }.
interpretation "Not member of" 'not_member_of x A =
(cic:/matita/logic/connectives/Not.con
notation "hvbox(x break ∉ A)" with precedence 60
for @{ 'not_member_of $x $A }.
interpretation "Not member of" 'not_member_of x A =
(cic:/matita/logic/connectives/Not.con