[STATEMENT]
lemma sngr_same_false[simp]: 
  "p \<mapsto>\<^sub>r x * p \<mapsto>\<^sub>r y = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<mapsto>\<^sub>r x * p \<mapsto>\<^sub>r y = false
[PROOF STEP]
unfolding times_assn_def bot_assn_def sngr_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (times_assn_raw (Rep_assn (Abs_assn (sngr_assn_raw p x))) (Rep_assn (Abs_assn (sngr_assn_raw p y)))) = Abs_assn (\<lambda>_. False)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. False = (h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn (Abs_assn (sngr_assn_raw p x))) (Rep_assn (Abs_assn (sngr_assn_raw p y)))))
[PROOF STEP]
apply (auto simp: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done