Got 'sorted_tree t <==> sorted_tree (tree_insert n t)' working. Now trying to get the less simplified definition of leftmost_leq working with this.