Satisfied Policies is ok

theorem satisfiedPolicies_is_ok (effect : Effect) {ps ps' : Policies} {Γ : TypeEnv}  (hwf : Γ.WellFormed)  (hwt : wellTypedPolicies ps Γ = .ok ps') :  ∃ asserts, satisfiedPolicies effect ps' (SymEnv.ofEnv Γ) = .ok asserts:= by  simp only [SymCC.satisfiedPolicies]  have ⟨ts, hts⟩ :    ∃ ts,      List.filterMapM (fun x => compileWithEffect effect x (SymEnv.ofEnv Γ)) ps' = .ok ts  := by    induction ps' generalizing ps with    | nil => exists []    | cons hd tl ih =>      simp only [List.filterMapM_cons]      have hwt_policies := List.mapM_ok_implies_all_from_ok hwt      have ⟨p, hmem_p, hwt_p⟩ := hwt_policies hd List.mem_cons_self      have ⟨asserts, hasserts⟩ := compileWithEffect_is_ok effect hwf hwt_p      simp only [hasserts, bind_pure_comp, Except.bind_ok]      cases ps with      | nil => contradiction      | cons ps_hd ps_tl =>        simp only [wellTypedPolicies, List.mapM_cons, bind, Except.bind, pure, Except.pure] at hwt        split at hwt        contradiction        split at hwt        contradiction        rename_i heq        simp only [Except.ok.injEq, List.cons.injEq] at hwt        simp only [hwt.2] at heq        have ⟨ts_tl, hts_tl⟩ := ih heq        split        · exists ts_tl        · simp [hts_tl]  simp [hts]