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