proposition: Lemma randomPerm_bad_preserves_wf_pair : forall ls d p, well_formed_Bvector_perm ls -> In p (getSupport (randomPerm_bad (ls, d))) -> well_formed_Bvector_perm (fst p).
proof: Proof. intuition. destruct p. eapply randomPerm_bad_preserves_wf; eauto. Qed.
imports: Crypto Permutation Broken.ConstructedFunc State FCF