proposition: Theorem comp_spec_impl_eq : forall (A B : Set){eqda : EqDec A}{eqdb : EqDec B}(c1 : Comp A)(c2 : Comp B), forall x y, comp_spec (fun a b => a = x <-> b = y) c1 c2 -> evalDist c1 x == evalDist c2 y.
proof: Proof. intuition. eapply leRat_impl_eqRat. eapply comp_spec_impl_le. eapply comp_spec_consequence. eauto. intuition. subst. intuition. eapply comp_spec_impl_le. eapply comp_spec_symm. eapply comp_spec_consequence. eauto. intuition. subst. intuition. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1