notation "'Ext' \sub b" non associative with precedence 90 for @{'ext $b}.
notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}.
interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 ? ? (or_f_minus ? ?) (Orel x)).
notation "'Ext' \sub b" non associative with precedence 90 for @{'ext $b}.
notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}.
interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 ? ? (or_f_minus ? ?) (Orel x)).