proposition: Lemma randomPerm_preserves_wf_pair : forall ls d p, well_formed_perm ls -> In p (getSupport (randomPerm (ls, d))) -> well_formed_perm (fst p).
proof: Proof. intuition. destruct p. eapply randomPerm_preserves_wf; eauto. Qed.
imports: Crypto Permutation CompFold Array FCF State