proposition: Lemma nth_app : forall (l m: list A) a i, nth_error (l ++ m) i = Some a -> (nth_error l i = Some a /\ i < length l) \/ (nth_error m (i - length l) = Some a /\ i >= length l).
proof: Proof. intros. destruct (le_lt_dec (length l) i). right; split; trivial. rewrite (nth_app_right l m l0) in H; trivial. left; split; trivial. rewrite (nth_app_left l m l0) in H; trivial. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)