proposition: Lemma term_size_many_app M Ns : term_size (many_app M Ns) = list_sum (map (fun N => S (term_size N)) Ns) + term_size M.
proof: Proof. elim: Ns M. - done. - move=> ?? IH ? /=. rewrite IH /=. lia. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect