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