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