[STATEMENT]
lemma class_add_relevant_entries:
 "\<not> is_class P C
  \<Longrightarrow> set (relevant_entries P i pc xt) \<subseteq> set (relevant_entries (class_add P (C, cdec)) i pc xt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_class P C \<Longrightarrow> set (relevant_entries P i pc xt) \<subseteq> set (relevant_entries (class_add P (C, cdec)) i pc xt)
[PROOF STEP]
by(clarsimp simp: relevant_entries_def class_add_is_relevant_entry)