proposition: Theorem evalDist_event_equiv : forall (A : Set){eqd : EqDec A}(c : Comp A) a, evalDist c a == Pr[x <-$ c; ret (eqb a x)].
proof: Proof. intuition. destruct (in_dec (EqDec_dec _) a (getSupport c)). rewrite evalDist_seq_step. rewrite (@sumList_exactly_one _ a). dist_compute. eapply getSupport_NoDup. trivial. intuition. dist_compute. rewrite evalDist_seq_step. assert (evalDist c a == 0). eapply getSupport_not_In_evalDist; trivial. rewrite H. symmetry. eapply sumList_0. intuition. dist_compute. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1