proposition: Lemma trace_mutex'_locked_extend : forall tr h n, trace_mutual_exclusion' h tr -> last_holder' h tr = None -> trace_mutual_exclusion' h (tr ++ [(Client n, inr [Locked])]).
proof: Proof. Proof using. induction tr; intros; simpl in *. - subst. auto. - simpl in *. repeat break_match; subst; intuition. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)