proposition: Lemma trace_order_total A (t : trace A) (ND : trace_nodup t) : is_total (trace_elems t) (trace_order t).
proof: Proof. red; ins. apply trace_in_nth with (d := a) in IWa; desf. apply trace_in_nth with (d := a) in IWb; desf. destruct (lt_eq_lt_dec n n0) as [[LT|]|LT]; desf; try congruence. left; repeat eexists; eauto. right; repeat eexists; eauto using trace_nth_indep. rewrite trace_nth_indep with (d' := a); ins. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription