proposition: Lemma contender_4''_reification_helper: exists res, interp_term nil res = existT _ tpNat contender_4''.
proof: Proof. eexists. unfold contender_4''. repeat t. all: reflexivity. Defined.
imports: Arith Lia List FunctionalExtensionality