proposition: Lemma getUnusedR_ret_preserves_wf : forall ls ls' d r, well_formed_perm ls -> ls#d = None -> In (ls', r) (getSupport (r <-$ getUnusedR ls; ret ((d, r) :: ls, r))) -> well_formed_perm ls'.
proof: Proof. intuition. apply getSupport_Bind_In in H1. destruct H1. intuition. simpl in H3. intuition. inversion H1; clear H1; subst. eapply getUnusedR_preserves_wf; eauto. Qed.
imports: Crypto Permutation CompFold Array FCF State