proposition: Lemma replace_at_pos_unfold : forall f l u i q, replace_at_pos (Term f l) u (i :: q) = Term f (replace_at_pos_list l u i q).
proof: Proof. intros f l u i q; simpl; apply (f_equal (fun l => Term f l)); generalize u i q; clear u i q; induction l as [| t l]; intros u i q; trivial. simpl; destruct i as [ | i ]; trivial. rewrite <- IHl; trivial. Qed.
imports: List more_list list_permut list_set Arith