proposition: Theorem step_failure_dup_drop_step : forall ps ps' Sigma f, dup_drop_step_star _ ps ps' -> step_failure_star (f, mkNetwork ps Sigma) (f, mkNetwork ps' Sigma) [].
proof: Proof. Proof using. induction 1. - constructor. - match goal with | [ H : dup_drop_step _ _ _ |- _ ] => invc H end. + find_apply_lem_hyp in_split. break_exists. break_and. subst. apply refl_trans_n1_1n_trace. eapply RTn1TStep with (cs := []). * apply refl_trans_1n_n1_trace. apply IHclos_refl_trans_n1. * eapply StepFailure_dup; [simpl; eauto|]. auto. + apply refl_trans_n1_1n_trace. eapply RTn1TStep with (cs := []). * apply refl_trans_1n_n1_trace. apply IHclos_refl_trans_n1. * eapply StepFailure_drop; [simpl; eauto|]. auto. Qed.
imports: Coq(List Relations Permutation) StructTact(StructTactics) Verdi(Net)