proposition: Lemma max_size_app l l' : max_size (l ++ l') = Nat.max (max_size l) (max_size l').
proof: Proof. induction l; simp max_size. reflexivity. simpl. rewrite <- Nat.max_assoc. f_equal. apply IHl. Qed.
imports: Program Equations(Equations) Utf8 Lia Arith List