Unfold Not in conclusions of forward rules?

[JLimperg]

The forward rule

@[aesop safe destruct] theorem not_prime_one : ¬Prime 1

(taken from Mathlib) currently means that in any context, ¬Prime 1 should be added as a hypothesis. But it was perhaps intended to mean that in a context with h : Prime 1, Aesop should derive False.

Possible actions:

• When adding a forward rule, unfold a leading Not in the conclusion. It should be possible to disable this behaviour via a builder option since adding a forward rule with negative conclusion is not necessarily wrong.
• Warn when adding a forward rule with a negated conclusion.

[JLimperg]

Also, forward rules with conclusion False and no non-immediate premises should always use destruct since there's no reason to keep the matched hyps around. Or there could be special support that lets forward rules with conclusion False immediately close the goal.