proposition: Lemma natPlus (a b : nat): SysPrf NN (natToTerm a + natToTerm b = natToTerm (a + b)%nat)%fol.
proof: Proof. induction b as [| b Hrecb]. - rewrite Nat.add_comm; cbn; apply nn3. - rewrite Nat.add_comm; cbn. apply eqTrans with (Succ (natToTerm a + natToTerm b))%fol. + apply nn4. + apply eqSucc. rewrite Nat.add_comm; apply Hrecb. Qed.
imports: Coq(Arith Lia) hydras.Ackermann(folLogic3 folProp subProp) hydras.Ackermann(folLogic3 folProp subProp) hydras(Compat815)