proposition: Theorem nestedRandomFunc_wf : forall (ls s : list (D * R)) d, well_formed_comp (nestedRandomFunc ls s d).
proof: Proof. intros. unfold nestedRandomFunc. destruct (arrayLookup _ ls d); wftac. eapply randomFunc_wf. trivial. Qed.
imports: FCF.FCF FCF.CompFold FCF.Array FCF.Hybrid