proposition: Theorem rndListElem_support_None : forall (A : Set) eqd (ls : list A), In None (getSupport (rndListElem eqd ls)) <-> ls = nil.
proof: Proof. intuition. unfold rndListElem in *. case_eq (length ls); intuition. destruct ls; simpl in *; trivial; discriminate. rewrite H0 in H. repeat simp_in_support. apply RndNat_support_lt in H1. edestruct (nth_option_some ls); eauto. rewrite H0. eauto. congruence. subst. simpl. intuition. Qed.
imports: FCF.FCF