proposition: Lemma element_at_app_r : forall l l' p, p >= length l -> (l ++ l') [p] = l' [p - length l].
proof: Proof. induction l. intuition. intros. destruct p. inversion H. simpl. apply IHl. simpl in H. auto with arith. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)