Partial `aesop?` should be able to close goals with unsafe rules

[JLimperg]

Via Zulip: when aesop doesn't fully solve a goal, aesop? currently generates a script that applies exactly the safe prefix of rules. However, we could additionally apply unsafe rules to subgoals that were ultimately fully solved. Note: we may need to apply these rules before script extraction, similar to ExtractSafeGoals.