proposition: Theorem constant_cost_bind_const1 : forall (A : Type)(B C: Set) (f1 : Comp B)(f2 : A -> B -> Comp C) c1 c2, cost f2 c1 -> (forall a, cost (f2 a) c2) -> cost (fun a => Bind f1 (f2 a)) (c1 + c2).
proof: Proof. intuition. eapply constant_cost_le. eapply constant_cost_bind; eauto. eapply constant_cost_const. lia. Qed.
imports: FCF.Crypto