proposition: Theorem lowDistApprox_Ret_inv : forall (A : Set)(eqd : eq_dec A)(a a' : A) n v, lowDistApprox (Ret eqd a) a' n v -> v == (if (eqd a a') then 1 else 0).
proof: Proof. intuition. destruct H. destruct H. intuition. specialize (map_Ret_repeat H0); intuition. subst. destruct (eqd a a'); subst. specialize (pred_count_listRepeat_eq_inv _ H); intuition. subst. rewrite H2. rewrite getAllBlists_length. eapply num_dem_same_rat1. trivial. specialize (@pred_count_listRepeat_ne_inv (length (getAllBlists n)) _ (ca_done a') (ca_done a) x0); intuition. rewrite H1 in H2. rewrite H2. apply rat_num_0. intuition. inversion H3. intuition. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat