proposition: Lemma boundedLT (m : nat) (a : Formula) (x : nat): (forall n : nat, n < m -> SysPrf NN (substF a x (natToTerm n))) -> SysPrf NN (v#x < natToTerm m -> a)%fol.
proof: Proof. revert m a x; simple induction m; intros. apply impI. apply contradiction with (v# x < natToTerm 0)%fol. - apply Axm; right; constructor. - apply sysWeaken, nn7. - apply impI; eapply orE. + apply impE with (v#x < natToTerm (S n))%fol. * apply sysWeaken; cbn; apply nn8. * apply Axm; right; constructor. + apply sysWeaken, H. intros n0 H1; apply H0. apply Nat.lt_lt_succ_r; auto. + apply sysWeaken, impI. rewrite <- (subFormulaId LNN a x). apply impE with (substF a x (natToTerm n)). * apply (subWithEquals LNN). apply eqSym. apply Axm; right; constructor. * apply sysWeaken, H0. apply Nat.lt_succ_diag_r . Qed.
imports: Coq(Arith Lia) hydras.Ackermann(folLogic3 folProp subProp) hydras.Ackermann(folLogic3 folProp subProp) hydras(Compat815)