proposition: Lemma pa2 (a b : Term): SysPrf PA (Succ a = Succ b -> a = b)%nt.
proof: Proof. set (m := fun x : nat => match x with | O => a | S _ => b end) in *. replace (Succ a = Succ b -> a = b)%nt with (subAllFormula LNT (Succ v#0 = Succ v#1 -> v#0 = v#1)%nt (fun x : nat => match le_lt_dec 2 x with | left _ => var x | right _ => m x end)). - apply (subAllCloseFrom LNT). simpl; apply Axm; repeat (try right; constructor) || left. - simpl; induction (le_lt_dec 2 0). + lia. + destruct (le_lt_dec 2 1). * lia. * reflexivity. Qed.
imports: Coq(Arith Lia Ensembles Decidable) hydras.Ackermann(folProp subAll folLogic3) hydras.Ackermann(NewNotations)