fact: Definition subst_in_sp p1 p2 sp := let pair_1 := partition_sp_1 p2 sp in let sp_to_modify := fst_sp(pair_1) in let sp_to_keep := snd_sp(pair_1) in let pair_2 := partition_sp_2 p2 sp_to_modify in let sp_to_modify_f := fst_sp(pair_2) in let sp_to_modify_s := snd_sp(pair_2) in let newsp_to_modify_f := SP.fold (subst_in_sp_aux_1 p1) sp_to_modify_f SP.empty in let newsp_to_modify_s := SP.fold (subst_in_sp_aux_2 p1) sp_to_modify_s SP.empty in SP.union (SP.union newsp_to_modify_f newsp_to_modify_s) sp_to_keep.
imports: Recdef NArith GeoCoq.Utils.sets