proposition: Lemma nn7 (a : Term): SysPrf NN (~ (a <Zero))%fol.
proof: Proof. change (~ (a <Zero))%fol with (substF (~ v#0 < 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)