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