[STATEMENT]
lemma pat_rule:
  "\<lbrakk> p\<equiv>p'; ID p' t' T \<rbrakk> \<Longrightarrow> ID p t' T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<equiv> p'; ID p' t' T\<rbrakk> \<Longrightarrow> ID p t' T
[PROOF STEP]
by simp