proposition: Theorem cost_compose_unary : forall (A B C: Type) (f1 : A -> B)(f2 : B ->C) c1 c2, cost f1 c1 -> cost f2 c2 -> cost (fun a => f2 (f1 a)) (c1 + c2).
proof: Proof. intuition. eapply cost_le. eapply (cost_compose f1 _ ). eauto. intuition. eapply cost_const. intuition. eauto. lia. Qed.
imports: FCF.FCF FCF.Admissibility