proposition: Lemma last_holder'_neq_unlock_extend : forall tr h n c, last_holder' h tr = Some n -> n <> c -> last_holder' h (tr ++ [(Client c, inl Unlock)]) = Some n.
proof: Proof. Proof using. induction tr; intros; simpl in *; repeat break_match; subst; try congruence; intuition. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)