proposition: Lemma element_at_not_replaced : forall l p q a, p <> q -> l[p] = l[q:=a][p].
proof: Proof. intro l; induction l as [ | h t IHl]; intros p q a p_neq_q; simpl. trivial. destruct p as [ | p']. destruct q as [ | q']; simpl. elim p_neq_q; trivial. trivial. destruct q as [ | q']; simpl. trivial. apply IHl. intro H; apply p_neq_q; subst; trivial. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)