proposition: Theorem rndListElem_support_exists : forall (A : Set)(eqd : EqDec A)(ls : list A), exists x, In x (getSupport (rndListElem eqd ls)).
proof: Proof. destruct ls; intuition. econstructor. left. eauto. unfold rndListElem. unfold length. econstructor. eapply getSupport_In_Seq. eapply (@in_getSupport_RndNat O). lia. simpl. intuition. Qed.
imports: FCF.FCF