proposition: Lemma trace_nth_map (n : nat) A B (f : B -> A) (t : trace B) d : trace_nth n (trace_map f t) (f d) = f (trace_nth n t d).
proof: Proof. destruct t; ins; apply map_nth. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription