proposition: Lemma log_step_failure_star_simulation : forall net failed tr, step_failure_disk_ops_star step_failure_disk_ops_init (failed, net) tr -> step_failure_star step_failure_init (failed, revertLogNetwork net) tr.
proof: Proof. Proof using. intros net failed tr H_star. remember step_failure_disk_ops_init as y in *. change failed with (fst (failed, net)). change net with (snd (failed, net)) at 2. revert Heqy. induction H_star using refl_trans_1n_trace_n1_ind; intro H_init. - find_rewrite. simpl; unfold revertLogNetwork; simpl. unfold step_failure_init, step_async_init. constructor. - concludes. destruct x' as (failed', net'). destruct x'' as (failed'', net''). subst. apply RT1n_step with (y := (failed', revertLogNetwork net')). + apply IHH_star1. + eapply log_step_failure_step; eauto. Qed.
imports: Verdi(Verdi) Cheerios(Cheerios) Verdi(Log) Coq(FunctionalExtensionality)