proposition: Theorem evalDist_bool_equiv_all : forall (c1 c2 : Comp bool), well_formed_comp c1 -> well_formed_comp c2 -> Pr[c1] == Pr[c2] -> (forall b, evalDist c1 b == evalDist c2 b).
proof: Proof. intuition. destruct b. trivial. rewrite evalDist_complement. rewrite evalDist_complement. eapply ratSubtract_eqRat_compat; intuition. trivial. trivial. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia