proposition: Lemma datRepeat_left_total : forall n (A : Set)(eqd : eq_dec A)(t : DistApproxTree A)(f : DistApproxTree A -> Prop) P, (exists b : DistApproxTree A, f b) -> exists t', datRepeat f P n t t'.
proof: Proof. induction n. induction t; intuition. destruct o. case_eq (P a); intuition. econstructor. econstructor. trivial. econstructor. eapply datRepeat_leaf_Some_no. trivial. econstructor. econstructor. edestruct IHt1. eauto. edestruct IHt2. eauto. econstructor. econstructor; eauto. induction t; intuition. destruct o. destruct H. edestruct (IHn _ eqd x). eauto. case_eq (P a); intuition. econstructor. econstructor. trivial. edestruct IHn; eauto. econstructor. eapply datRepeat_leaf_Some_repeat. eauto. trivial. eauto. econstructor. econstructor. edestruct IHt1; eauto. edestruct IHt2; eauto. econstructor. econstructor; eauto. Unshelve. trivial. eapply P. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat