Opt satisfied Policies correctness

theorem Opt.satisfiedPolicies.correctness (effect : Effect) (ps : Policies) (εnv : SymEnv) :  Opt.satisfiedPolicies effect ps εnv = (do    let term ← SymCC.satisfiedPolicies effect ps εnv    let footprint := footprints (ps.filterMap λ p => if p.effect = effect then p.toExpr else none) εnv    .ok { term, footprint }  ):= by  simp [Opt.satisfiedPolicies, SymCC.satisfiedPolicies]  have := filterMapM_compileWithEffect_correctness effect ps εnv  simp_do_let ps.filterMapM (Opt.compileWithEffect effect · εnv)  case error e h =>    specialize this [] -- doesn't matter what we choose in this case    simp_all [Except.map, ← this]  case ok ress hress =>    specialize this ress    simp_all [Except.map, ← this.left, footprints]    conv => lhs ; rw [List.mapUnion_eq_mapUnion_id_map]    simp [this, List.mapUnion_filterMap]    apply List.mapUnion_congr    intro p hp    simp only [Option.mapD, id_eq]    grind