[STATEMENT]
lemma opt_mru_guard_imp_Quorum:
  "opt_mru_guard vs Q v \<Longrightarrow> Q \<in> Quorum"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. opt_mru_guard vs Q v \<Longrightarrow> Q \<in> Quorum
[PROOF STEP]
by (simp add: opt_mru_guard_def Let_def)