proposition: Theorem low_tree_approx_same_inv : forall n (A : Set)(eqd : eq_dec A)(c : Comp A)(t : DistApproxTree A) (a : A) r, dat_correct c n t -> lowDistApprox c a n r -> lowDistApproxFromTree eqd t a == r.
proof: Proof. intuition. eapply low_tree_approx_same_inv_h. eauto. eapply lowDistApprox_ls_impl. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat