proposition: Theorem comp_spec_consequence : forall (A B : Set){eqda1 eqda2 : EqDec A}{eqdb1 eqdb2 : EqDec B}(p1 p2 : A -> B -> Prop) c1 c2, (@comp_spec _ _ eqda1 eqdb1 p1 c1 c2) -> (forall a b, p1 a b -> p2 a b) -> (@comp_spec _ _ eqda2 eqdb2 p2 c1 c2).
proof: Proof. intuition. despec; intuition. exists x; intuition. rewrite H1. unfold marginal_l. dist_skip. eapply evalDist_ret_eq. case_eq (eqb (fst x0) r1); intuition. rewrite eqb_leibniz in H4. subst. eapply eqb_refl. case_eq ( (@eqb A eqda1 (@fst A B x0) r1)); intuition. rewrite eqb_leibniz in H5. subst. rewrite eqb_refl in H4. intuition. rewrite H. unfold marginal_r. dist_skip. eapply evalDist_ret_eq. case_eq (eqb (snd x0) r2); intuition. rewrite eqb_leibniz in H4. subst. eapply eqb_refl. case_eq ( (@eqb B eqdb1 (@snd A B x0) r2)); intuition. rewrite eqb_leibniz in H5. subst. rewrite eqb_refl in H4. intuition. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1