proposition: Theorem rndListElem_pred : forall (A B : Set)(eqda : EqDec A)(eqdb : EqDec B)(P : A -> B -> Prop)(lsa : list A)(lsb : list B), list_pred P lsa lsb -> comp_spec (fun a b => match a with | None => b = None | Some a' => exists b', b = Some b' /\ P a' b' end) (rndListElem _ lsa) (rndListElem _ lsb).
proof: Proof. intuition. unfold rndListElem in *. case_eq (length lsa); intuition. erewrite <- list_pred_length_eq; eauto. rewrite H0. eapply comp_spec_ret; intuition. erewrite <- list_pred_length_eq; eauto. rewrite H0. comp_skip. apply None. apply None. eapply comp_spec_ret; intuition. case_eq (nth_option lsa b); intuition. edestruct list_pred_nth_exists; eauto. exfalso. eapply nth_option_not_None; eauto. apply RndNat_support_lt in H1. lia. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation