proposition: Theorem primary_ge_backup : forall net tr, step_async_star (params := Counter_MultiParams) step_async_init net tr -> nwState net backup <= nwState net primary.
proof: Proof. intros. apply backup_plus_network_eq_primary in H. auto with *. Qed.
imports: Verdi(Verdi HandlerMonad)