proposition: Lemma randomFunc_eager_preserves_bad : forall ls d ls' r, In (ls', r) (getSupport (randomFunc_eager (ls, d))) -> checkBad ls = true -> checkBad ls' = true.
proof: Proof. intuition. unfold randomFunc_eager in *. simp_in_support. case_eq (ls # d); intuition; rewrite H in H2; simp_in_support. rewrite checkBad_app_cons; simpl. rewrite H0. eapply orb_true_r. rewrite checkBad_app_cons; simpl. rewrite H0. eapply orb_true_r. Qed.
imports: Crypto Permutation Broken.ConstructedFunc State FCF