Cpset sat Asserts Opt? eqv sat Asserts? ok

theorem cpset_satAssertsOpt?_eqv_satAsserts?_ok {pss wpss : List Policies} {cpsets : List CompiledPolicySet} {Γ : Validation.TypeEnv} :  pss.length = cpsets.length →  cpsets ≠ [] →  pss.mapM (CompiledPolicySet.compile · Γ) = .ok cpsets →  pss.mapM (wellTypedPolicies · Γ) = .ok wpss →  satAsserts? wpss.flatten asserts (SymEnv.ofTypeEnv Γ) = satAssertsOpt? (cpsets.map CompiledPolicies.pset) asserts:= by  intro hlen  simp [satAsserts?, satAssertsOpt?]  intro hnil hcpsets hwpss  have hεnv : ∀ cpset ∈ cpsets, cpset.εnv = SymEnv.ofTypeEnv Γ := by    intro cpset hcpset    replace ⟨ps, hps, hcpsets⟩ := List.mapM_ok_implies_all_from_ok hcpsets cpset hcpset    exact cpset_compile_produces_the_right_env hcpsets  revert hnil  cases cpsets <;> simp  case cons cpset cpsets =>  cases pss <;> simp at *  case cons ps pss =>  simp [do_eq_ok] at hwpss hcpsets  replace ⟨wps, hwps, hwpss⟩ := hwpss  simp [Functor.map, Except.map] at hwpss  split at hwpss <;> simp at hwpss  subst wpss ; rename_i wpss hwpss  replace ⟨cpset', hcpset', hcpsets⟩ := hcpsets  simp [Functor.map, Except.map] at hcpsets  split at hcpsets <;> simp at hcpsets  replace ⟨hcpsets, htemp⟩ := hcpsets ; subst cpset' htemp ; rename_i cpsets hcpsets ; have hcpset := hcpset' ; clear hcpset'  simp only [CompiledPolicies.εnv]  rw [cpset_compile_produces_the_right_env hcpset]  congr  funext I  cases I <;> simp only  case some I =>  suffices SymEnv.extract? (List.map (List.map Policy.toExpr) (wps :: wpss)).flatten I (SymEnv.ofTypeEnv Γ) = extractOpt? (.pset cpset :: cpsets.map CompiledPolicies.pset) I by rw [this] ; rfl  rw [extractOpt?_eqv_extract? (εnv := cpset.εnv) (by simp)]  · congr 1    · simp only [List.map_cons, List.flatten_cons, List.flatMap_cons, CompiledPolicies.allPolicies,        List.map_append]      simp only [flatMap_allPolicies_policies]      congr 2      · simp [cpset_compile_produces_the_right_policies hcpset hwps]      · simp [List.flatMap]        congr 1        rw [← List.forall₂_iff_map_eq]        apply List.Forall₂.imp (R := λ a b => a = CompiledPolicySet.policies b)        · intro a b h ; subst h ; simp        · rw [List.mapM_ok_iff_forall₂] at hcpsets hwpss          apply List.forall₂_trans_ish hwpss hcpsets          intro ps wps cpset hwps hcpset          exact (cpset_compile_produces_the_right_policies hcpset hwps).symm    · simp [cpset_compile_produces_the_right_env hcpset]  · intro cps hcps    cases hcps    · rfl    · rename_i hcps      change cps ∈ cpsets.map CompiledPolicies.pset at hcps      simp only [List.mem_map] at hcps      replace ⟨cpset', hcpset', hcps⟩ := hcps ; subst cps      replace ⟨hεnv, hεnv'⟩ := hεnv      simp [CompiledPolicies.εnv, hεnv, hεnv' cpset' hcpset']  · intro cps hcps    cases hcps    · exists ps, Γ    · rename_i hcps      change cps ∈ cpsets.map CompiledPolicies.pset at hcps      simp only [List.mem_map] at hcps      replace ⟨cpset', hcpset', hcps⟩ := hcps ; subst cps      replace ⟨ps', hps', hcpsets⟩ := List.mapM_ok_implies_all_from_ok hcpsets cpset' hcpset'      exists ps', Γ