proposition: Lemma upperbound_eval: forall t, eval t <= eval (largest_of_depth (term_depth t)).
proof: Proof. intros. unfold largest_of_depth. eapply Nat.le_trans. 2: { eapply lowerbound_maxBy with (x := t). 2: reflexivity. eapply termsUpTo_correct. lia. } lia. Qed.
imports: Arith Lia List FunctionalExtensionality