proposition: Lemma trace_order_trans A (t : trace A) x y z : trace_order t x y -> trace_order t y z -> trace_order t x z.
proof: Proof. unfold trace_order; splits; ins; desf. rewrite trace_nth_indep with (d' := x) in *; ins; eauto. 2: destruct (trace_length t); ins; lia. exists i0, j; splits; eauto. destruct (le_lt_dec j0 i) as [|LT]; try lia. exfalso; eapply H0; try apply LT; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription