proposition: Lemma LTS_trace_prefix_closed t t' : LTS_trace t' -> trace_prefix t t' -> LTS_trace t.
proof: Proof. destruct t, t'; ins; desf; exists fl'; splits; ins. all: specialize (H1 i); rewrite ?length_app in *. all: specialize_full H1; try lia. all: try rewrite nth_app in *; desf; eauto; try lia. rewrite <- H0; ins. rewrite H0; ins. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription