proposition: Lemma trace_nth_in A (t : trace A) n (LT : NOmega.lt_nat_l n (trace_length t)) d : trace_elems t (trace_nth n t d).
proof: Proof. destruct t; ins; desf; eauto using nth_In. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription