proposition: Lemma getUnusedR_wf : forall ls r, inRange ls r = false -> In r (getSupport RndR) -> well_formed_comp (getUnusedR ls).
proof: Proof. intuition. unfold getUnusedR. eapply (well_formed_Repeat _ _ r). wftac. eapply filter_In. intuition. rewrite H. simpl. trivial. Grab Existential Variables. unfold eq_dec; intuition. eapply (EqDec_dec _). Qed.
imports: Crypto Permutation CompFold Array FCF State