proposition: Lemma trace_mutex'_unlock_extend : forall tr h c, trace_mutual_exclusion' h tr -> trace_mutual_exclusion' h (tr ++ [(Client c, inl Unlock)]).
proof: Proof. Proof using. induction tr; intros; simpl in *; repeat break_match; intuition (auto; try congruence). Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)