[STATEMENT]
lemma ss_exps_throw_Val:
 "\<lbrakk> val_of e = \<lfloor>a\<rfloor>; ss_exps (map Val vs @ throw e # es') = \<lfloor>e'\<rfloor> \<rbrakk>
   \<Longrightarrow> e' = throw e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>val_of e = \<lfloor>a\<rfloor>; ss_exps (map Val vs @ throw e # es') = \<lfloor>e'\<rfloor>\<rbrakk> \<Longrightarrow> e' = throw e
[PROOF STEP]
by(induct vs) (auto)