[STATEMENT]
lemma psubst_new_subset:
  assumes \<open>set z \<subseteq> set z'\<close> \<open>c \<notin> (\<Union>p \<in> set z. params p)\<close>
  shows \<open>set z \<subseteq> set (map (psubst (id(c := n))) z')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set z \<subseteq> set (map (psubst (id(c := n))) z')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set z \<subseteq> set z'
c \<notin> \<Union> (params ` set z)

goal (1 subgoal):
 1. set z \<subseteq> set (map (psubst (id(c := n))) z')
[PROOF STEP]
by force


[STATEMENT]
lemma subset_cons: \<open>set z \<subseteq> set z' \<Longrightarrow> set (p # z) \<subseteq> set (p # z')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set z \<subseteq> set z' \<Longrightarrow> set (p # z) \<subseteq> set (p # z')
[PROOF STEP]
by auto