[STATEMENT]
lemma success_freezeI [success_intros]:
  "success (freeze a) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (freeze a) h
[PROOF STEP]
by (auto intro: success_intros simp add: freeze_def)