proposition: Lemma lowDistApprox_func : forall (A : Set)(c : Comp A) a n r1 r2, well_formed_comp c -> lowDistApprox c a n r1 -> lowDistApprox c a n r2 -> r1 == r2.
proof: Proof. intuition. edestruct (dat_exists). eauto. rewrite <- low_tree_approx_same_inv; eauto. eapply low_tree_approx_same_inv; eauto. Unshelve. eapply comp_eq_dec; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat