proposition: Theorem Repeat_body_eq : forall (A : Set) (eqda : EqDec A)(c1 c2 : Comp A) f, (forall x, evalDist c1 x == evalDist c2 x) -> (forall x, evalDist (Repeat c1 f) x == evalDist (Repeat c2 f) x).
proof: Proof. intros. destruct (in_dec (EqDec_dec _) x (getSupport c1)). case_eq (f x); intuition idtac. eapply evalDist_Repeat_eq; intuition idtac. eauto. eapply filter_In; intuition idtac. erewrite sumList_permutation. eapply sumList_body_eq. intuition idtac. eauto. apply evalDist_getSupport_filter_perm; intuition idtac. eauto. repeat rewrite evalDistRepeat_pred_0; intuition idtac. reflexivity. repeat rewrite evalDistRepeat_sup_0; intuition idtac. reflexivity. rewrite <- H. eapply getSupport_not_In_evalDist_h; eauto. eapply getSupport_not_In_evalDist_h; eauto. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms