Opt is Authorized correctness

theorem Opt.isAuthorized.correctness (ps : Policies) (εnv : SymEnv) :  Opt.isAuthorized ps εnv = (do    let term ← SymCC.isAuthorized ps εnv    let footprint := footprints (ps.map Policy.toExpr) εnv    .ok { term, footprint }  ):= by  simp [Opt.isAuthorized, SymCC.isAuthorized]  rw [Opt.satisfiedPolicies.correctness .permit]  rw [Opt.satisfiedPolicies.correctness .forbid]  simp_do_let SymCC.satisfiedPolicies .forbid ps εnv as hforbid  simp_do_let SymCC.satisfiedPolicies .permit ps εnv as hpermit  rename_i ft pt  simp only [Except.ok.injEq, Opt.CompileResult.mk.injEq, true_and]  simp only [footprints, List.mapUnion_filterMap, List.mapUnion_map]  rw [List.mapUnion_union_mapUnion']  · apply List.mapUnion_congr    intro p hp    cases p.effect <;> simp only [reduceCtorEq, ↓reduceIte, Option.mapD_none, Option.mapD_some, Function.comp_apply]    · exact Data.Set.union_empty_right (footprint_wf _ _)    · exact Data.Set.union_empty_left (footprint_wf _ _)  · intro p hp    cases p.effect <;> simp [Data.Set.empty_wf, footprint_wf _ _]