[STATEMENT]
lemma lift_lemma [simp]: \<open>\<lparr>E\<langle>0:x\<rangle>, F\<rparr> (\<^bold>\<up>t) = \<lparr>E, F\<rparr> t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>E\<langle>0:x\<rangle>, F\<rparr> (\<^bold>\<up> t) = \<lparr>E, F\<rparr> t
[PROOF STEP]
by (induct t) (auto cong: map_cong)