Additions to VCV-io's OracleComp.EvalDist

theorem OracleComp.support_ofFn_mapM_index {ι α : Type} {spec : OracleSpec ι} {L : ℕ} (f : Fin L → OracleComp spec α) {v : Vector α L} (hv : v ∈ support (Vector.mapM f (Vector.ofFn fun (i : Fin L) => i))) (i : Fin L) : v[i] ∈ support (f i)

Index-extraction for (Vector.ofFn id).mapM over an OracleComp: any element in the support of the monadic mapM has each component lying in the support of the corresponding inner computation.