proposition: Lemma nn2 (a b : Term): SysPrf NN (S_ a = S_ b -> a = b)%fol.
proof: Proof. set (m := fun x : nat => match x with | O => a | S _ => b end) in *. change (S_ a = S_ b -> a = b)%fol with (subAllFormula LNN (S_ v#0 = S_ v#1 -> v#0 = v#1)%fol (fun x : nat => match le_lt_dec 2 x with | left _ => var x | right _ => m x end)). - apply (subAllCloseFrom LNN). cbn; apply Axm; repeat (try right; constructor) || left. Qed.
imports: Coq(Arith Lia Ensembles List) hydras.Ackermann(folProp subAll folLogic3 Languages) hydras(Compat815 NewNotations)