proposition: Lemma randomPerm_preserves_wf : forall ls d ls' r, well_formed_perm ls -> In (ls', r) (getSupport (randomPerm (ls, d))) -> well_formed_perm ls'.
proof: Proof. intuition. unfold randomPerm in *. case_eq (ls#d); intuition. rewrite H1 in H0. simpl in *. intuition. inversion H2; clear H2; subst. trivial. rewrite H1 in H0. eapply getUnusedR_ret_preserves_wf; eauto. Qed.
imports: Crypto Permutation CompFold Array FCF State