fact: Fixpoint replace_at_pos_list (l : list term) (u : term) (i : nat) (p : list nat) {struct l}: list term := match l with | nil => nil | h :: tl => match i with | O => (replace_at_pos h u p) :: tl | S j => h :: (replace_at_pos_list tl u j p) end end.
imports: List more_list list_permut list_set Arith