proposition: Lemma replace_newer : forall (l : list A) (p : nat) (x x' : A), p < length l -> replace (replace l p x) p x' = replace l p x'.
proof: Proof. simple induction l. simpl in |- *. trivial with arith. simple induction p. simpl in |- *. intros. trivial with arith. intros. clear H0. simpl in |- *. rewrite H. trivial with arith. auto with arith. Qed.
imports: Lists_field