proposition: Lemma trace_prefix_trans A (t t' t'' : trace A) : trace_prefix t t' -> trace_prefix t' t'' -> trace_prefix t t''.
proof: Proof. destruct t, t', t''; ins; desf; try rewrite <- H0; eauto. by rewrite appA; vauto. forward apply H0 with (i := i) (d := d); rewrite ?length_app, ?nth_app; ins; desf; lia. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription