- simplify.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption.
- simplify.intro.apply (not_eq_pos_neg n1 n).apply sym_eq.assumption.
+ simplify.unfold Not.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption.
+ simplify.unfold Not.intro.apply (not_eq_pos_neg n1 n).apply sym_eq.assumption.