proposition: Lemma ack'_equiv: forall n a b, ack' n a b = ack n a b.
proof: Proof. induction n; intros; simpl. - reflexivity. - destruct n. + simpl. apply add'_equiv. + specialize (IHn a). rewrite <- (iter_proper _ _ IHn). rewrite <- iter'_equiv. reflexivity. Qed.
imports: Arith Lia List FunctionalExtensionality