proposition: Lemma trace_elems_nth A (t : trace A) d : trace_elems t ≡₁ (⋃₁ n ∈ (fun n => NOmega.lt_nat_l n (trace_length t)), eq (trace_nth n t d)).
proof: Proof. repeat autounfold with unfolderDb; intuition; desf; eauto using trace_in_nth with hahn. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription