[STATEMENT]
lemma gen'_cp_intros:
  "gen' y Q G \<Longrightarrow> gen' x (Conj Q (x \<approx> y)) ((\<lambda>Q. cp (Q[y \<^bold>\<rightarrow> x])) ` G)"
  "gen' y Q G \<Longrightarrow> gen' x (Conj Q (y \<approx> x)) ((\<lambda>Q. cp (Q[y \<^bold>\<rightarrow> x])) ` G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gen' y Q G \<Longrightarrow> gen' x (Conj Q (x \<approx> y)) ((\<lambda>Q. cp (Q[y \<^bold>\<rightarrow> x])) ` G)) &&& (gen' y Q G \<Longrightarrow> gen' x (Conj Q (y \<approx> x)) ((\<lambda>Q. cp (Q[y \<^bold>\<rightarrow> x])) ` G))
[PROOF STEP]
by (metis (no_types, lifting) gen'.intros(8) gen'_qp image_cong qp_cp_subst_triv,
      metis (no_types, lifting) gen'.intros(9) gen'_qp image_cong qp_cp_subst_triv)