Came up with the 'caseOfRec' floating step, which removes the need for subterm checking in fix-fact fusion. All tests passing, plus the two subgoals of 'sorted_tree t ==> sorted_tree (ins k t)'.