proposition: Lemma dat_correct_repeat_same: forall n (A : Set) (t : DistApproxTree A) (c : Comp A) (P : A -> bool), well_formed_comp c -> (exists a, In a (filter P (getSupport c))) -> dat_correct (Repeat c P) n t -> dat_correct_repeat c P n t.
proof: Proof. intuition. edestruct (dat_exists); eauto. econstructor. intuition. eauto. destruct H0. eapply dat_correct_repeat_same_h; eauto. intuition. rewrite firstn_nil in H3. eapply evalDet_nil. eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat