proposition: Lemma evalDet_lowDistApprox_ls_done_inv : forall (A : Set)(eqd : eq_dec A)(c : Comp A) s a1 a2 n r, evalDet c s (ca_done a1) -> lowDistApprox_ls c a2 n s r -> r == if (eqd a2 a1) then 1 else 0.
proof: Proof. intuition. destruct H0. destruct H0. intuition. destruct (eqd a2 a1); subst. rewrite <- H3. erewrite pred_count_eq_all_inv at 1. erewrite <- rel_map_length. rewrite getAllBlists_length. apply num_dem_same_rat1. unfold posnatToNat. unfold natToPosnat. eauto. eapply H1. eauto. intuition. eapply rel_map_unary_pred. eapply H1. intuition. eapply evalDet_app_eq in H. eapply evalDet_func; eauto. trivial. rewrite <- H3. erewrite pred_count_eq_0 at 1. apply rat_num_0. 2:{ eapply H1. } 2:{ eapply H0. } intuition. subst. eapply n0. assert (ca_done a1 = ca_done a2). eapply evalDet_func. eapply evalDet_app_eq. eauto. eauto. inversion H5. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat