proposition: Lemma datMap_depth_better : forall (A B : Set)(tb1 tb2 : DistApproxTree B), dat_better tb1 tb2 -> forall n1 n2 (f : nat -> B -> DistApproxTree A -> Prop) t1 t2, (forall n1 n2 b t1 t2, n1 >= n2 -> f n1 b t1 -> f n2 b t2 -> dat_better t1 t2) -> datMap (f n1) tb1 t1 -> datMap_depth f n2 tb2 t2 -> n1 >= n2 -> dat_better t1 t2.
proof: Proof. induction 1; intuition; simpl in *. inversion H1; clear H1; subst. econstructor. inversion H1; clear H1; subst. inversion H0; clear H0; subst. eauto. inversion H2; clear H2; subst. inversion H3; clear H3; subst. econstructor. eapply IHdat_better1; eauto; lia. eapply IHdat_better2; eauto; lia. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat