Implemented a new function for pushing fact contexts inwards in fix-fact fusion. It leaves a lot of crap around but it gets the job done, so I now have 'not sorted_tree(t) ==> not sorted_tree(t)' simplifying properly.