Refactored the appears_in_tree prop, and changed a ton of proofs to work with it.