fact: Fixpoint replace n (p : N -> bool) (v : N) l := match l with | a :: l1 => if p a then if n =? 0 then v :: l1 else a :: replace (n - 1) p v l1 else a :: replace n p v l1 | nil => nil end.
imports: Ascii String List EqNat NArith