[STATEMENT]
lemma pull_up_configuration_senior:
  "\<lbrakk>x \<in> configuration q n; y \<in> configuration q n\<rbrakk> \<Longrightarrow> senior x n = senior y n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> configuration q n; y \<in> configuration q n\<rbrakk> \<Longrightarrow> senior x n = senior y n
[PROOF STEP]
by force