proposition: Theorem randomFunc_lookup_Some_inv : forall (D R : Set)(eqdd : EqDec D)(rndR : Comp R) s1 s2 v x b a, In (v, s2) (getSupport (@randomFunc D R rndR _ s1 a)) -> arrayLookup _ s1 x = Some b -> arrayLookup _ s2 x = Some b.
proof: Proof. intuition idtac. unfold randomFunc in *. case_eq (arrayLookup eqdd s1 a); intuition idtac; rewrite H1 in H; repeat simp_in_support. trivial. simpl. case_eq (eqb x a); intuition idtac. rewrite eqb_leibniz in H. subst. rewrite H0 in H1. discriminate. Qed.
imports: FCF FCF.PRF Permutation