fact: Fixpoint replace_at_pos (t u : term) (p : list nat) {struct p} : term := match p with | nil => u | i :: q => match t with | Var _ => t | Term f l => let replace_at_pos_list := (fix replace_at_pos_list j (l : list term) {struct l}: list term := match l with | nil => nil | h :: tl => match j with | O => (replace_at_pos h u q) :: tl | S k => h :: (replace_at_pos_list k tl) end end) in Term f (replace_at_pos_list i l) end end.
imports: List more_list list_permut list_set Arith