Into Compiled Policy Set correctness

theorem intoCompiledPolicySet_correctness {p : Policy} {Γ : Validation.TypeEnv} :  (do    let cp ← CompiledPolicy.compile p Γ    pure cp.intoCompiledPolicySet  ) = CompiledPolicySet.compile [p] Γ:= by  simp [CompiledPolicy.compile, CompiledPolicySet.compile, CompiledPolicy.intoCompiledPolicySet, wellTypedPolicy_wellTypedPolicies, Except.mapError, Except.map]  cases wellTypedPolicy p Γ <;> simp  case ok p' =>  simp [Opt.isAuthorized, Opt.satisfiedPolicies, Opt.compileWithEffect]  cases p'.effect <;> simp [Factory.anyTrue, Factory.or, Factory.not, Factory.and]  all_goals {    simp_do_let Opt.compile p'.toExpr (SymEnv.ofEnv Γ) as h    simp only [Except.ok.injEq, CompiledPolicySet.mk.injEq, true_and]    have hwf := Opt.compile_footprint_wf h    simp [EmptyCollection.emptyCollection, Data.Set.union_empty_right List.mapUnion_wf, Data.Set.union_empty_left List.mapUnion_wf]    rw [List.mapUnion_singleton (by simp [hwf])]    simp  }