proposition: Lemma rndListElem_support: forall (A : Set)(eqd : EqDec A)(ls : list A) a, In a ls <-> In (Some a) (getSupport (rndListElem eqd ls)).
proof: Proof. intuition. unfold rndListElem. case_eq (length ls); intuition. exfalso. destruct ls; simpl in *; intuition. eapply getSupport_In_Seq. eapply in_getSupport_RndNat. rewrite <- H0. eapply firstIndexOf_in_lt; eauto. simpl. left. eapply nth_firstIndexOf; trivial. unfold rndListElem in *. repeat simp_in_support. discriminate. eapply nth_option_In; eauto. Unshelve. unfold eq_dec. eapply (EqDec_dec eqd). apply O. Qed.
imports: FCF.FCF