proposition: Lemma randomFunc_eager_wf : forall ls d, well_formed_comp (randomFunc_eager (ls, d)).
proof: Proof. intuition. unfold randomFunc_eager. wftac. intuition. destruct (ls # d); wftac. Qed.
imports: Crypto Permutation Broken.ConstructedFunc State FCF