fact: Parameter subst_replace_at_pos : forall t u p sigma, is_a_pos t p = true -> apply_subst sigma (replace_at_pos t u p) = replace_at_pos (apply_subst sigma t) (apply_subst sigma u) p.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)