-interpretation "Apartness alikeness" 'napart a b = (eq _ a b).
-interpretation "Excess alikeness" 'napart a b = (eq (excess_base_OF_excess1 _) a b).
-interpretation "Excess (dual) alikeness" 'napart a b = (eq (excess_base_OF_excess _) a b).
+interpretation "Apartness alikeness" 'napart a b = (eq ? a b).
+interpretation "Excess alikeness" 'napart a b = (eq (excess_base_OF_excess1 ?) a b).
+interpretation "Excess (dual) alikeness" 'napart a b = (eq (excess_base_OF_excess ?) a b).