proposition: Lemma ack_in_flight_to_primary_backup : forall p, pDst p = backup -> ack_in_flight_to_primary [p] = 0.
proof: Proof. intros. unfold ack_in_flight_to_primary. simpl. repeat break_match; try congruence; auto. Qed.
imports: Verdi(Verdi HandlerMonad)