proposition: Lemma evalDet_equiv_impl_lowDistApprox_equiv : forall (A : Set)(c1 c2 : Comp A), evalDet_equiv c1 c2 -> forall a n r, lowDistApprox c1 a n r <-> lowDistApprox c2 a n r.
proof: Proof. intuition. unfold lowDistApprox, evalDet_equiv in *. destruct H0. destruct H0. intuition. exists x. exists x0. intuition. eapply rel_map_impl. eapply H1. intuition. eapply H. trivial. unfold lowDistApprox, evalDet_equiv in *. destruct H0. destruct H0. intuition. exists x. exists x0. intuition. eapply rel_map_impl. eapply H1. intuition. eapply H. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat