proposition: Remark mapListLemma : forall l : list nat, fold_right Nat.max 0 (map S l) <= S (fold_right Nat.max 0 l).
proof: Proof. induction l as [| a l Hrecl]. - simpl; auto. - simpl; induction (fold_right Nat.max 0 (map S l)). + apply le_n_S. apply Nat.le_max_l. + apply le_n_S, maxLemma. * apply le_n. * now apply le_S_n. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)