proposition: Lemma trace_order_irrefl A (t : trace A) x (ORD: trace_order t x x) : False.
proof: Proof. unfold trace_order in *; ins; desf. eapply ORD with (d := x); eauto; congruence. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription