proposition: Remark boundSubFormulaHelp2 (a : fol.Formula L) (v0 : nat) (s : fol.Term L): newVar (v0 :: freeVarT s ++ freeVarF a) <= S (fold_right Nat.max 0 (v0 :: fold_right Nat.max 0 (freeVarT s) :: varFormula a)).
proof: Proof. unfold newVar; apply Nat.le_trans with (S (fold_right Nat.max 0 (v0 :: freeVarT s ++ freeVarF a))). - apply mapListLemma. - apply le_n_S; simpl; apply maxLemma. + apply le_n. + induction (maxApp (freeVarT s) (freeVarF a)) as [a0 | b]. * rewrite a0; apply Nat.le_max_l. * rewrite b; eapply Nat.le_trans. -- apply maxVarFreeVar. -- apply Nat.le_max_r. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)