proposition: Lemma interp_contender_4''_reified: projT2 (interp_term nil contender_4''_reified) = contender_4''.
proof: Proof. cbv -[Nat.recursion]. repeat apply f_equal. reflexivity. Qed.
imports: Arith Lia List FunctionalExtensionality