proposition: Theorem well_founded_subtree : well_founded subtree.
proof: Proof. intros t; induction t as [ | x t1 IHt1 t2 IHt2]. - split; inversion 1. - split; intros y Hsub; inversion_clear Hsub; assumption. Qed.
imports: Lia Inverse_Image Wellfounded.Inclusion Wf_nat