proposition: Lemma dat_better_antisymm : forall (A : Set)(t1 t2 : DistApproxTree A), dat_better t1 t2 -> dat_better t2 t1 -> t1 = t2.
proof: Proof. induction 1; inversion 1; intuition; subst; trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat