proposition: Lemma randomPerm_bad_wf : forall ls d, well_formed_Bvector_perm ls -> well_formed_comp (randomPerm_bad (ls, d)).
proof: Proof. intuition. unfold randomPerm_bad. case_eq (ls#d); intuition. wftac. wftac. Qed.
imports: Crypto Permutation Broken.ConstructedFunc State FCF