proposition: Lemma trace_order_in1 A (t : trace A) a b : trace_order t a b -> trace_elems t a.
proof: Proof. unfold trace_order; destruct t; ins; desf; ins; eauto. rewrite <- H2; apply nth_In; lia. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription