Methods for expression reduction check and theorem-style substitution validation

[aethesia]

Is there a convenient way to determine if two expressions can be reduced to the same form?

Additionally, is there a method to check if an expression can be substituted/applied as a theorem to another expression? I am looking for something similar to the have tactic, but which returns a boolean value instead of throwing an error.

The standard == function only checks for structural equality and lacks the ability to perform stronger automatic expansion.

[uniwuni]

just had the same issue, the definitional expansion would already help quite a bit