proposition: Lemma datMap_better : forall (A B : Set)(t : DistApproxTree B) n (rel : nat -> B -> DistApproxTree A -> Prop) t1 t2, (forall n b t1 t2, rel n b t1 -> rel (pred n) b t2 -> dat_better t1 t2) -> datMap (rel n) t t1 -> datMap (rel (pred n)) t t2 -> dat_better t1 t2.
proof: Proof. induction t; intuition; simpl in *. inversion H0; clear H0; subst. inversion H1; clear H1; subst. econstructor. inversion H1; clear H1; subst. eapply H; eauto. inversion H0; clear H0; subst. inversion H1; clear H1; subst. econstructor; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat