proposition: Theorem randomFunc_hist_wf : forall ls d, well_formed_comp (randomFunc_hist ls d).
proof: Proof. unfold randomFunc_hist. intuition idtac. destruct (arrayLookup _ ls d); wftac. Qed.
imports: FCF.FCF FCF.CompFold FCF.Array FCF.Hybrid