proposition: Lemma ordered_dynamic_nodes_no_dup : forall onet failed tr, step_ordered_dynamic_failure_star step_ordered_dynamic_failure_init (failed, onet) tr -> NoDup (odnwNodes onet).
proof: Proof. Proof using. move => net failed tr H. remember step_ordered_dynamic_failure_init as y in *. have ->: net = snd (failed, net) by []. move: Heqy. induction H using refl_trans_1n_trace_n1_ind => H_init. rewrite H_init /=. exact: NoDup_nil. concludes => {H_init}. match goal with | [ H : step_ordered_dynamic_failure _ _ _ |- _ ] => invc H end; rewrite //=. exact: NoDup_cons. Qed.
imports: Verdi(Verdi) StructTact(Update) Coq(FunctionalExtensionality) Coq(Sumbool Relation_Definitions RelationClasses) Verdi(Ssrexport)