[STATEMENT]
lemma app_insf2_Seq: "Seq s k \<Longrightarrow> k' \<noteq> k \<Longrightarrow> app (insf s k y) k' = app s k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Seq s k; k' \<noteq> k\<rbrakk> \<Longrightarrow> app (insf s k y) k' = app s k'
[PROOF STEP]
by (simp add: app_nonrestrict_Seq insf_def app_ins2)