proposition: Lemma induct (f : Formula) (v : nat): let f_0 := substF f v Zero in let f_Sv := substF f v (Succ (v#v))%nt in SysPrf PA f_0 -> SysPrf PA (allH v, f -> f_Sv)%nt -> SysPrf PA (allH v, f)%nt.
proof: Proof. intros ? ? H H0; eapply impE. - eapply impE. + apply (openClosed LNT). apply Axm; repeat left. unfold InductionSchema in |- *. unfold In in |- *. unfold PA7 in |- *. exists f, v; reflexivity. + apply H. - apply H0. Qed.
imports: Coq(Arith Lia Ensembles Decidable) hydras.Ackermann(folProp subAll folLogic3) hydras.Ackermann(NewNotations)