Proved find_subtree_after_replace except for three small admits
Merged.. Me and morten did the same easy proof