proposition: Lemma nth_app_l {A} (a : A) {n} (l l' : list A) : n < length l -> nth n (l @ l') a = nth n l a.
proof: Proof. revert l l' n; induction l; intros; auto. depelim H. destruct n; trivial. simpl. eapply IHl. simpl in H. lia. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia