proposition: Lemma dat_exists_repeat2 : forall (A : Set)(c : Comp A)(P : A -> bool)(n : nat), well_formed_comp c -> exists t : DistApproxTree A, dat_correct_repeat2 c P n t.
proof: Proof. intuition. destruct (@dat_exists n _ c). trivial. edestruct (@datRepeat_left_total n A (comp_eq_dec c) x (dat_correct c n) P). eapply dat_exists; eauto. econstructor. unfold dat_correct_repeat2. econstructor. intuition. eauto. eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat