proposition: Theorem evalDist_right_ident_eqb : forall (A : Set)(eqd : EqDec A)(c : Comp A)(a : A), Pr[x <-$ c; ret (eqb a x)] == evalDist c a.
proof: Proof. intuition. symmetry. rewrite <-(@evalDist_right_ident _ eqd). comp_skip. simpl. repeat match goal with |- context [ if ?X then _ else _ ] => destruct X end; rewrite ?@eqb_leibniz in *; reflexivity || congruence. Qed.
imports: FCF.FCF FCF.CompFold