proposition: Theorem constant_cost_bind_const1_pair : forall (A : Type)(B C: Set) (f1 : Comp B)(f2 : A -> B -> Comp C) c, cost (fun p => f2 (fst p) (snd p)) c -> cost (fun a => Bind f1 (f2 a)) c.
proof: Proof. intuition. apply constant_cost_pair_args in H0. destruct H0. destruct H0. intuition. eapply constant_cost_le. eapply constant_cost_bind; eauto. eapply constant_cost_const. lia. Qed.
imports: FCF.Crypto