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