proposition: Lemma NN2PA (f : fol.Formula LNN): folProof.SysPrf LNN NN f -> SysPrf PA (LNN2LNT_formula f).
proof: Proof. intro H; apply translateProof with NN. - apply closedPA1. - intros f0 H0; unfold NN in H0. destruct H0 as [x H0| x H0]. + destruct H0 as [x H0| x H0]. * destruct H0 as [x H0| x H0]. -- destruct H0 as [x H0| x H0]. ++ destruct H0 as [x H0| x H0]. ** destruct H0 as [x H0| x H0]. destruct H0 as [x H0| x H0]. destruct H0 as [x H0| x H0]. destruct H0. apply Axm; repeat (try right; constructor) || left. destruct H0. apply Axm; repeat (try right; constructor) || left. destruct H0. apply Axm; repeat (try right; constructor) || left. destruct H0. apply Axm; repeat (try right; constructor) || left. ** destruct H0. apply Axm; repeat (try right; constructor) || left. ++ destruct H0. apply Axm; repeat (try right; constructor) || left. -- destruct H0. apply NN72PA. * destruct H0. apply NN82PA. + destruct H0. apply NN92PA. - apply H. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(folProp folProof subProp folLogic3 folReplace NN PAtheory) hydras.Ackermann(subAll ListExt)