proposition: Lemma L1: RepresentableHalf1 NN 1 (fun n => n + n) (v#0 = v#1 + v#1)%fol.
proof: Proof. intro a; simpl. pose (H:= natPlus a a). unfold substF; simpl. apply impI. apply eqTrans with (natToTerm a + natToTerm a)%fol. - apply sysExtend with (Ensembles.Singleton _ (v#0 = natToTerm a + natToTerm a)%fol). + right; assumption. + apply Axm; split. - eapply sysExtend with NN. + left; assumption. + apply H. Qed.
imports: hydras.Ackermann(expressible) hydras.Ackermann(NN NewNotations NNtheory) Coq(Lia)