proposition: Lemma pa1 (a : Term): SysPrf PA (Succ a <> Zero)%nt.
proof: Proof. replace (Succ a <> Zero)%nt with (substF (Succ v#0 <> Zero)%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)