Theory Solve_Cong

subsection ‹Setup for the Heap Monad›

theory Solve_Cong
  imports Main "HOL-Eisbach.Eisbach"
begin

text ‹Method for solving trivial equalities with congruence reasoning›

named_theorems cong_rules

method solve_cong methods solve =
  rule HOL.refl |
  rule cong_rules; solve_cong solve |
  solve; fail

end