proposition: Lemma L4 : Representable NN 1 (fun n => n * 2) (v#0 = v#1 + v#1)%fol.
proof: Proof. split. simpl; lia. apply Representable_ext with (fun n => n + n). - intro n. simpl. lia. - apply L3. Qed.
imports: hydras.Ackermann(expressible) hydras.Ackermann(NN NewNotations NNtheory) Coq(Lia)