proposition: Lemma AckSn_as_PRiterate (n:nat): extEqual 1 (Ack (S n)) (fun k => primRec.iterate (Ack n) (S k) 1).
proof: Proof. intros k; rewrite AckSn_as_iterate. generalize (Ack n); intro f. generalize 1; generalize (S k); induction n0. - cbn; auto. - cbn; intro n1; rewrite IHn0; auto. Qed.
imports: hydras(primRec Ack MoreVectors) Coq(Arith ArithRing List Lia Compare_dec)