proposition: Theorem eq_impl_comp_spec_eq : forall (A : Set){eqd1 eqd2 : EqDec A}(c1 c2 : Comp A), (forall x, evalDist c1 x == evalDist c2 x) -> @comp_spec _ _ eqd1 eqd2 eq c1 c2.
proof: Proof. intuition. exists (x <-$ c1; ret (x, x)). intuition. unfold marginal_l. dist_inline_first. rewrite <- evalDist_right_ident. dist_skip. dist_compute. unfold marginal_r. dist_inline_first. rewrite <- H. rewrite <- evalDist_right_ident. dist_skip. dist_compute. repeat simp_in_support. trivial. Unshelve. intuition. intuition. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1