[STATEMENT]
lemma prec_frame:
  assumes PREC: "precise P"
  assumes M1: "h\<Turnstile>(R1 \<and>\<^sub>A R2)"
  assumes F1: "R1 \<Longrightarrow>\<^sub>A P x p * F1"
  assumes F2: "R2 \<Longrightarrow>\<^sub>A P y p * F2"
  shows "x=y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
using preciseD[OF PREC] M1 F1 F2
[PROOF STATE]
proof (prove)
using this:
?h \<Turnstile> P ?a ?p * ?F \<and>\<^sub>A P ?a' ?p * ?F' \<Longrightarrow> ?a = ?a'
h \<Turnstile> R1 \<and>\<^sub>A R2
R1 \<Longrightarrow>\<^sub>A P x p * F1
R2 \<Longrightarrow>\<^sub>A P y p * F2

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (metis entailsD mod_and_dist)