proposition: Theorem constant_cost_compose_binary : forall (A B C D: Type) (f1 : A -> B)(f2 : A ->C)(f3 : B -> C -> D) c1 c2 c3 c4, cost f1 c1 -> cost f2 c2 -> cost f3 c3 -> (forall b, cost (f3 b) c4) -> cost (fun a => f3 (f1 a) (f2 a)) (c1 + c2 + c3 + c4).
proof: Proof. intuition. eapply constant_cost_le. eapply (constant_cost_compose f2 (fun a x => f3 (f1 a) x)). eauto. eapply (constant_cost_compose f1 (fun a y x => f3 y x)). eauto. eapply constant_cost_const. intuition. eauto. intuition. lia. Qed.
imports: FCF.Crypto