fact: Definition subst_in_ss p1 p2 ss := let pair := partition_ss p2 ss in let fss := fst_ss(pair) in let sss := snd_ss(pair) in let newfss := SS.fold (subst_in_ss_aux p1 p2) fss SS.empty in SS.union newfss sss.
imports: Recdef NArith GeoCoq.Utils.sets