Revert "a proof for tej"
Revert "a proof for tej"

This reverts commit 720bdb1aafa5deb0501d14a65d815ca25234f7f2.

Frans points out this theorem is already there, called [find_subtree_app']

mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl