proposition: Theorem comp_spec_eq_symm: forall (A : Set){eqda : EqDec A}(c1 c2 : Comp A), comp_spec eq c1 c2 -> comp_spec eq c2 c1.
proof: Proof. intuition. eapply comp_spec_symm. eapply comp_spec_consequence; eauto. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1