fact: Fixpoint replace (l : list A) : nat -> A -> list A := fun (position : nat) (new : A) => match l return (list A) with | nil => nil | x :: l' => match position return (list A) with | O => new :: l' | S n' => x :: replace l' n' new end end.
imports: Lists_field