proposition: Theorem randomFunc_mem_wf : forall (A B : Set) x y z (w : list (A * B)) v, well_formed_comp z -> well_formed_comp (randomFunc_mem x y z w v).
proof: Proof. intuition. unfold randomFunc_mem. destruct (arrayLookup x w v); intuition; wftac. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv