proposition: Theorem F_randomFunc_wf : forall x y z, well_formed_comp (F_randomFunc x y z).
proof: Proof. intuition. unfold F_randomFunc. destruct (arrayLookup_f _ y (F x z)); wftac. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv