proposition: Lemma dat_repeat_better: forall (A : Set) n (c : Comp A) (P : A -> bool) (t1 t2 : DistApproxTree A), (exists a : A, In a (filter P (getSupport c))) -> dat_correct_repeat c P n t1 -> dat_correct_repeat2 c P n t2 -> dat_better t2 t1.
proof: Proof. intuition. unfold dat_correct_repeat, dat_correct_repeat2 in *. destruct H0. destruct H1. intuition. eapply datRepeat_better_depth. eauto. eauto. eapply dat_correct_dat_better. eauto. eauto. lia. lia. lia. intuition. eapply dat_correct_dat_better; eauto. intuition. inversion H1; clear H1; subst. inversion H7; clear H7; subst. destruct H. assert (x1 = a). eapply evalDet_steps_nil_eq; eauto. eapply filter_In; eauto. subst. eapply filter_In; eauto. intuition. destruct H. eapply datCorrect_datDepth. eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat