proposition: Lemma getUnusedR_preserves_wf : forall ls d r, well_formed_perm ls -> ls#d = None -> In r (getSupport (getUnusedR ls)) -> well_formed_perm ((d, r) :: ls).
proof: Proof. intuition. unfold getUnusedR in *. simpl in H1. apply filter_In in H1. intuition. eapply well_formed_perm_cons; eauto. destruct (inRange ls r); simpl in *; congruence. Qed.
imports: Crypto Permutation CompFold Array FCF State