proposition: Lemma nn3 (a : Term): SysPrf NN (a + Zero = a)%fol.
proof: Proof. change (a + Zero = a)%fol with (substF (v#0 + Zero = v#0)%fol 0 a). - apply forallE; apply Axm; repeat (try right; constructor) || left. Qed.
imports: Coq(Arith Lia Ensembles List) hydras.Ackermann(folProp subAll folLogic3 Languages) hydras(Compat815 NewNotations)