proposition: Lemma trace_prefix_refl A (t : trace A) : trace_prefix t t.
proof: Proof. destruct t; ins; eauto using app_nil_end. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription