proposition: Lemma evalDist_Repeat_eq : forall (A : Set)(c1 c2 : Comp A)(P1 P2 : A -> bool) v1 v2, evalDist c1 v1 == evalDist c2 v2 -> P1 v1 = P2 v2 -> In v1 (filter P1 (getSupport c1)) -> sumList (filter P1 (getSupport c1)) (evalDist c1) == sumList (filter P2 (getSupport c2)) (evalDist c2) -> evalDist (Repeat c1 P1) v1 == evalDist (Repeat c2 P2) v2.
proof: Proof. intuition. simpl. eapply ratMult_eqRat_compat; intuition. eapply ratMult_eqRat_compat. unfold indicator. rewrite H0. intuition. eapply ratInverse_eqRat_compat. intuition. eapply getSupport_In_evalDist. eapply filter_In. eauto. eapply sumList_0 in H3; eauto. trivial. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia