proposition: Lemma dat_better_refl : forall (A : Set)(t : DistApproxTree A), dat_better t t.
proof: Proof. induction t; intuition. destruct o; econstructor. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat