proposition: Theorem constant_cost_pair_args_weak : forall (A B C : Type) (f : A -> B -> C) c, cost (fun p => f (fst p) (snd p)) c -> cost f c.
proof: Proof. intuition. apply constant_cost_pair_args in H0. destruct H0. destruct H0. intuition. eapply constant_cost_le. eauto. lia. Qed.
imports: FCF.Crypto