proposition: Theorem dat_exists : forall n (A : Set)(c : Comp A), well_formed_comp c -> exists t : DistApproxTree A, dat_correct c n t.
proof: Proof. intuition. eapply dat_exists_h. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat