Cp sat Asserts Opt? eqv sat Asserts? ok

theorem cp_satAssertsOpt?_eqv_satAsserts?_ok {ps wps : Policies} {cps : List CompiledPolicy} {Γ : Validation.TypeEnv} :  ps.length = cps.length →  cps ≠ [] →  ps.mapM (CompiledPolicy.compile · Γ) = .ok cps →  ps.mapM (wellTypedPolicy · Γ) = .ok wps →  satAsserts? wps asserts (SymEnv.ofTypeEnv Γ) = satAssertsOpt? (cps.map CompiledPolicies.policy) asserts:= by  intro hlen  simp [satAsserts?, satAssertsOpt?]  intro hnil hcps hwps  have hεnv : ∀ cp ∈ cps, cp.εnv = SymEnv.ofTypeEnv Γ := by    intro cp hcp    replace ⟨p, hp, hcps⟩ := List.mapM_ok_implies_all_from_ok hcps cp hcp    exact cp_compile_produces_the_right_env hcps  revert hnil  cases cps <;> simp  case cons cp cps =>  cases ps <;> simp at *  case cons p ps =>  simp [do_eq_ok] at hwps hcps  replace ⟨wp, hwp, hwps⟩ := hwps  simp [Functor.map, Except.map] at hwps  split at hwps <;> simp at hwps  subst wps ; rename_i wps hwps  replace ⟨cp', hcp', hcps⟩ := hcps  simp [Functor.map, Except.map] at hcps  split at hcps <;> simp at hcps  replace ⟨hcps, htemp⟩ := hcps ; subst cp' htemp ; rename_i cps hcps ; have hcp := hcp' ; clear hcp'  simp only [CompiledPolicies.εnv]  rw [cp_compile_produces_the_right_env hcp]  congr  funext I  cases I <;> simp only  case some I =>  suffices SymEnv.extract? ((wp :: wps).map Policy.toExpr) I (SymEnv.ofTypeEnv Γ) = extractOpt? (.policy cp :: cps.map CompiledPolicies.policy) I by rw [this] ; rfl  rw [extractOpt?_eqv_extract? (εnv := cp.εnv) (by simp)]  · congr 1    · simp only [List.map_cons, List.flatMap_cons, CompiledPolicies.allPolicies,        List.cons_append, List.nil_append, List.cons.injEq]      simp only [flatMap_allPolicies_policy, List.map_map]      simp only [cp_compile_produces_the_right_policy hcp hwp, true_and]      rw [← List.forall₂_iff_map_eq]      apply List.Forall₂.imp (R := λ a b => a = b.policy)      · intro a b h ; subst a ; simp      · rw [List.mapM_ok_iff_forall₂] at hcps hwps        apply List.forall₂_trans_ish hwps hcps        intro p wp cp hwp hcp        exact (cp_compile_produces_the_right_policy hcp hwp).symm    · simp [cp_compile_produces_the_right_env hcp]  · intro cps' hcps'    cases hcps'    · rfl    · rename_i hcps'      change cps' ∈ cps.map CompiledPolicies.policy at hcps'      simp only [List.mem_map] at hcps'      replace ⟨cp', hcp', hcps'⟩ := hcps' ; subst cps'      replace ⟨hεnv, hεnv'⟩ := hεnv      simp [CompiledPolicies.εnv, hεnv, hεnv' cp' hcp']  · intro cps' hcps'    cases hcps'    · exists p, Γ    · rename_i hcps'      change cps' ∈ cps.map CompiledPolicies.policy at hcps'      simp only [List.mem_map] at hcps'      replace ⟨cp', hcp', hcps'⟩ := hcps' ; subst cps'      simp only      replace ⟨p', hp', hcps⟩ := List.mapM_ok_implies_all_from_ok hcps cp' hcp'      exists p', Γ