proposition: Theorem comp_spec_eq_impl_eq : forall (A : Set){eqd1 eqd2 : EqDec A}(c1 c2 : Comp A), @comp_spec _ _ eqd1 eqd2 eq c1 c2 -> (forall x, evalDist c1 x == evalDist c2 x).
proof: Proof. intuition. despec. intuition. rewrite H0. rewrite H. unfold marginal_l, marginal_r. dist_skip. simpl. specialize (H2 x1). intuition. destruct x1. simpl in *. subst. destruct (EqDec_dec bool_EqDec (@eqb _ eqd1 a0 x) true); intuition. rewrite eqb_leibniz in e. subst. destruct (EqDec_dec bool_EqDec (@eqb _ eqd2 x x) true); intuition. exfalso. eapply n. eapply eqb_refl. destruct (EqDec_dec bool_EqDec (@eqb _ eqd2 a0 x) true); intuition. rewrite eqb_leibniz in e. subst. exfalso. eapply n. eapply eqb_leibniz. trivial. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1