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