proposition: Theorem GenRP_bad_wf : forall a b, (length (fst a) <= A2_queries)%nat -> well_formed_comp (GenRP_bad a b).
proof: Proof. intuition. simpl in *. case_eq (arrayLookup eqdd a0 b0); intuition; wftac. unfold rndNotBad; wftac. edestruct goodExists ; eauto. intuition. econstructor. unfold eq_dec; intuition. eapply (EqDec_dec _). trivial. eapply filter_In; intuition. eauto. rewrite H4. trivial. Qed.
imports: FCF PRF RndInList