fact: Parameter well_formed_replace_at_pos : forall p t u, well_formed t -> well_formed u -> well_formed (replace_at_pos t u p).
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)