We want to simplify this formula.
We can assume the formulas in the frame context.
Let us apply the SimplifyAuto tactic.
The SimplifyAuto tactic recursively simplifies the subformulas.
Tactic application successful. We get a simpler formula.
Let us see the proof information.
Three theorem provers have been tried to discharge this proof obligation.
This proof obligation has been discharged successfully by Alt-Ergo.
In one step, we got a much simpler formula.