proposition: Lemma pa3 (a : Term): SysPrf PA (a + Zero = a)%nt.
proof: Proof. replace (a + Zero = a)%nt with (substF (v#0 + Zero = v#0)%nt 0 a). - apply forallE, Axm; repeat (try right; constructor) || left. - reflexivity. Qed.
imports: Coq(Arith Lia Ensembles Decidable) hydras.Ackermann(folProp subAll folLogic3) hydras.Ackermann(NewNotations)