proposition: Lemma contender_4''_equiv: contender_4'' = contender_4.
proof: Proof. etransitivity. 2: exact contender_4'_equiv. unfold contender_4'', contender_4'. unfold ack'. repeat apply f_equal. reflexivity. Qed.
imports: Arith Lia List FunctionalExtensionality