proposition: Lemma element_at_replaced : forall l p a, p < length l -> l[p:=a][p] = Some a.
proof: Proof. intro l; induction l as [ | h t IHl]; simpl; intros p a Hlength. inversion Hlength. destruct p as [ | p]; simpl. trivial. apply IHl; gen Hlength; auto with arith. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)