proposition: Lemma L3: Representable NN 1 (fun n => n + n) (v#0 = v#1 + v#1)%fol.
proof: Proof. split. simpl. lia. apply RepresentableHalfHelp. apply L1. apply L2. Qed.
imports: hydras.Ackermann(expressible) hydras.Ackermann(NN NewNotations NNtheory) Coq(Lia)