proposition: Lemma trace_mutex'_no_out_extend : forall tr n h, trace_mutual_exclusion' h tr -> trace_mutual_exclusion' h (tr ++ [(n, inr [])]).
proof: Proof. Proof using. induction tr; intuition; unfold trace_mutual_exclusion in *; simpl in *; repeat break_match; subst; intuition. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)