proposition: Lemma getUnusedR_not_inRange : forall ls d r, ls#d = None -> In r (getSupport (getUnusedR ls)) -> inRange ls r = false.
proof: Proof. intuition. unfold getUnusedR in *. simpl in *. eapply filter_In in H0. intuition. destruct (inRange ls r); intuition. Qed.
imports: Crypto Permutation CompFold Array FCF State