proposition: Theorem reachable_revert : true_in_reachable step_dup step_async_init (fun st => reachable step_async step_async_init (revertNetwork st)).
proof: Proof. Proof using. apply true_in_reachable_reqs. - unfold revertNetwork. simpl. unfold reachable. exists []. constructor. - intros. find_apply_lem_hyp reachable_revert_step; auto. intuition. + unfold reachable in *. break_exists. eexists. apply refl_trans_n1_1n_trace. econstructor; eauto using refl_trans_1n_n1_trace. + find_rewrite. auto. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)