proposition: Theorem true_in_reachable_transform : forall P, true_in_reachable step_async step_async_init P -> true_in_reachable step_dup step_async_init (fun net => P (revertNetwork net)).
proof: Proof. Proof using. intros. find_apply_lem_hyp true_in_reachable_elim. intuition. apply true_in_reachable_reqs; eauto. intros. find_copy_apply_lem_hyp reachable_revert. find_apply_lem_hyp reachable_revert_step; auto. intuition. - break_exists. eauto. - repeat find_rewrite. auto. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)