proposition: Lemma lowDistApprox_ls_impl : forall n (A : Set)(c : Comp A) a r, lowDistApprox c a n r -> lowDistApprox_ls c a n nil r.
proof: Proof. intuition. destruct H. destruct H. intuition. econstructor. econstructor. intuition. simpl. eapply rel_map_eq. eapply H0. eauto. intuition. eauto. intuition. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat