proposition: Lemma trace_nth_app (n : nat) A (t t' : trace A) (d : A) : trace_nth n (trace_app t t') d = ifP NOmega.lt_nat_l n (trace_length t) then trace_nth n t d else trace_nth (NOmega.sub_nat_l n (trace_length t)) t' d.
proof: Proof. destruct t, t'; ins; unfold trace_prepend in *; desf; try rewrite app_nth; desf; auto using nth_indep; lia. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription