proposition: Lemma trace_nth_indep (n : nat) A (t : trace A) (LT : NOmega.lt_nat_l n (trace_length t)) (d d' : A) : trace_nth n t d = trace_nth n t d'.
proof: Proof. destruct t; ins; desf; auto using nth_indep. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription