proposition: Theorem contender_4_lt_contender_5 : contender_4 < contender_5.
proof: Proof. rewrite <- contender_4''_equiv. rewrite <- eval_contender_4''_reified. unfold contender_5, largest_STLCNatRec_nat_of_depth. eapply Nat.le_lt_trans. - eapply upperbound_eval. - eapply largest_of_depth_strictly_monotone. cbv. lia. Qed.
imports: Arith Lia List FunctionalExtensionality