proposition: Lemma lowDistApprox_val_eq : forall (A : Set)(c : Comp A) a n r1 r2, lowDistApprox c a n r1 -> r1 == r2 -> lowDistApprox c a n r2.
proof: Proof. intuition. unfold lowDistApprox in *. destruct H. destruct H. intuition. econstructor. econstructor. intuition. eauto. eauto. rewrite <- H0. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat