proposition: Theorem comp_spec_symm : forall (A B : Set){eqda : EqDec A}{eqdb : EqDec B}(p : A -> B -> Prop) c1 c2, comp_spec p c1 c2 -> comp_spec (fun b a => p a b) c2 c1.
proof: Proof. intuition. despec; intuition. exists (p <-$ x; ret (snd p, fst p)). intuition. eapply eqRat_trans; eauto. unfold marginal_r, marginal_l. dist_inline_first. dist_skip. dist_compute. eapply eqRat_trans; eauto. unfold marginal_r, marginal_l. dist_inline_first. dist_skip. dist_compute. repeat simp_in_support. simpl. eauto. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1