proposition: Lemma L2: RepresentableHalf2 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 + a)). - apply sysExtend with (Ensembles.Singleton _ (v#0 = natToTerm (a + a))%fol). + right. assumption. + apply Axm; split. - eapply sysExtend with NN. + left; assumption. + apply eqSym. apply H. Qed.
imports: hydras.Ackermann(expressible) hydras.Ackermann(NN NewNotations NNtheory) Coq(Lia)