[STATEMENT]
lemma restrict_relp_cong:
  "\<lbrakk> P = P'; Q = Q'; \<And>x y. \<lbrakk> P x; Q y \<rbrakk> \<Longrightarrow> R x y = R' x y \<rbrakk> \<Longrightarrow> R \<upharpoonleft> P \<otimes> Q = R' \<upharpoonleft> P' \<otimes> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P = P'; Q = Q'; \<And>x y. \<lbrakk>P x; Q y\<rbrakk> \<Longrightarrow> R x y = R' x y\<rbrakk> \<Longrightarrow> R \<upharpoonleft> P \<otimes> Q = R' \<upharpoonleft> P' \<otimes> Q'
[PROOF STEP]
by(auto simp add: fun_eq_iff)