proposition: Lemma trace_in_nth A (t : trace A) a (IN : trace_elems t a) d : exists n, NOmega.lt_nat_l n (trace_length t) /\ trace_nth n t d = a.
proof: Proof. destruct t; ins; desf; eauto using In_nth. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription