proposition: Lemma randomFunc_preserves_bad : forall ls ls' v r, checkBad ls = true -> In (ls', r) (getSupport (randomFunc_Bvector (ls, v))) -> checkBad ls' = true.
proof: Proof. intuition. unfold randomFunc_Bvector, randomFunc in *. case_eq (ls # v); intuition; rewrite H1 in H0. simp_in_support. trivial. repeat simp_in_support. simpl. rewrite H. eapply orb_true_r. Qed.
imports: Crypto Permutation Broken.ConstructedFunc State FCF