let apply_subst sigma a = TimerApply.start (); if Variable.is_subst_identity sigma then (TimerApply.pause (); a) else let a' = Array.init (Array.length a) (fun i -> Atom.subst sigma a.(i)) in Array.fast_sort Atom.compare a'; TimerApply.pause (); a'