[STATEMENT]
lemma ignores_old_varsD:
  "ignores_old_vars P \<Longrightarrow> length mdss = length mdss' \<Longrightarrow> length mdss' = length cms \<Longrightarrow>
  (map (\<lambda>x m. x m \<inter> (- range var\<^sub>C_of)) mdss) = (map (\<lambda>x m. x m \<inter> (- range var\<^sub>C_of)) mdss') \<Longrightarrow> 
  P mdss = P mdss'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ignores_old_vars P; length mdss = length mdss'; length mdss' = length cms; map (\<lambda>x m. x m \<inter> - range var\<^sub>C_of) mdss = map (\<lambda>x m. x m \<inter> - range var\<^sub>C_of) mdss'\<rbrakk> \<Longrightarrow> P mdss = P mdss'
[PROOF STEP]
unfolding ignores_old_vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>mdss mdss'. length mdss = length mdss' \<and> length mdss' = length cms \<longrightarrow> map (\<lambda>x m. x m \<inter> - range var\<^sub>C_of) mdss = map (\<lambda>x m. x m \<inter> - range var\<^sub>C_of) mdss' \<longrightarrow> P mdss = P mdss'; length mdss = length mdss'; length mdss' = length cms; map (\<lambda>x m. x m \<inter> - range var\<^sub>C_of) mdss = map (\<lambda>x m. x m \<inter> - range var\<^sub>C_of) mdss'\<rbrakk> \<Longrightarrow> P mdss = P mdss'
[PROOF STEP]
by force