1 2 3 4 5 6 7
(* optimize_heap should not affect the proof state *) Goal True. idtac. Show. optimize_heap. Show.