proposition: Lemma nth_app_left : forall (l m: list A) i, i < length l -> nth_error (l ++ m) i = nth_error l i.
proof: Proof. induction l; simpl; intros m i i_l. lia. destruct i; simpl. trivial. apply (IHl m i). auto with arith. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)