proposition: Lemma replace_at_app_r : forall l l' p a, p >= length l -> (l ++ l') [p := a] = l ++ l' [p - length l := a].
proof: Proof. induction l; intros. simpl. rewrite Nat.sub_0_r. refl. destruct p. inversion H. simpl. rewrite IHl. refl. intuition. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)