proposition: Remark R1 : extEqual 1 (Ack (S n)) (fun a : nat => nat_rec (fun _ : nat => nat) 1 (fun _ y : nat => Ack n y) (S a)).
proof: Proof. intro a; cbn; now rewrite iterate_nat_rec. Qed.
imports: hydras(primRec Ack MoreVectors) Coq(Arith ArithRing List Lia Compare_dec)