proposition: Lemma evalDistRepeat_pred_0 : forall (A : Set)(c : Comp A)(P : A -> bool) x, P x = false -> evalDist (Repeat c P) x == 0.
proof: Proof. intuition. simpl. unfold indicator. rewrite H. repeat rewrite ratMult_0_l. intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms