fact: Parameter 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).
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)