proposition: Lemma trace_order_nth_nth A (t : trace A) n (LTn : NOmega.lt_nat_l n (trace_length t)) d m (LTm : NOmega.lt_nat_l m (trace_length t)) d' : trace_order t (trace_nth n t d) (trace_nth m t d') <-> trace_nodup t /\ n < m.
proof: Proof. unfold trace_order; split; ins; desf; splits; ins. apply trace_nodup_inj in H2; ins; desf. apply trace_nodup_inj in H3; ins; desf. destruct (trace_length t); ins; lia. exists n, m; splits; ins; auto using trace_nth_indep. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription