proposition: Theorem lifting_applied : forall (net : @network _ PB_multi_params) tr, step_async_star step_async_init net tr -> trace_correct (revert_trace (base_params := vard_base_params) tr).
proof: Proof. apply transformer. eauto using step_1_star_trace_correct. Qed.
imports: Verdi(Verdi) Coq(String) Verdi(VarD PrimaryBackup)