Aesop internal error related to normalization

Stream: new members

[Pranav cs22b015]

While proving a relatively large theorem, I get the following error message:
aesop: internal error during proof reconstruction: goal 75 was not normalised.
Is there a way to fix this error?

Also, I have also got this error:
aesop: error in norm simp: simp failed: maximum number of steps exceeded
Is there a way to configure aesop to help avoid these?

[Vlad]

MWE:

import Mathlib

example {x y : Bool} {b : ℕ → Bool} :
(if b 1 || b 2 then some x else if b 3 then some x else none) =
(if b 4 || b 5 then none else if b 6 || b 7 then some y
else if b 8 then some y else none) := by
  aesop -- internal error during proof reconstruction: goal 6 was not normalised.