proposition: Theorem comp_spec_ret : forall (A B : Set){eqda1 : EqDec A}{eqdb1 : EqDec B}(eqda2 : eq_dec A)(eqdb2 : eq_dec B)(P : A -> B -> Prop) a b, P a b -> @comp_spec _ _ eqda1 eqdb1 P (Ret eqda2 a) (Ret eqdb2 b).
proof: Proof. intuition. exists (ret (a, b)). intuition. unfold marginal_l. dist_compute. unfold marginal_r. dist_compute. simp_in_support. trivial. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1