proposition: Lemma dat_better_trans : forall (A : Set)(t1 t2 : DistApproxTree A), dat_better t1 t2 -> forall t3, dat_better t2 t3 -> dat_better t1 t3.
proof: Proof. induction 1; intuition. inversion H; clear H; subst; eauto with dat. inversion H1; clear H1; subst. econstructor. econstructor; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat