proposition: Lemma trace_elems_app A (t t' : trace A) : trace_elems (trace_app t t') ≡₁ trace_elems t ∪₁ ifP trace_finite t then trace_elems t' else ∅.
proof: Proof. unfold set_union, trace_finite; split; intro x; rewrite trace_in_app; ins; desf; desf; ins; eauto. destruct t; ins; destruct n; eauto. right; ins. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription