Check Matches Implies Opt eqv check Matches Implies

theorem checkMatchesImpliesOpt_eqv_checkMatchesImplies {p₁ p₂ : Policy} {Γ : Validation.TypeEnv} :  Γ.WellFormed →  (do    let cp₁ ← CompiledPolicy.compile p₁ Γ    let cp₂ ← CompiledPolicy.compile p₂ Γ    pure $ checkMatchesImpliesOpt cp₁ cp₂  ) =  (do    let wp₁ ← wellTypedPolicy p₁ Γ |>.mapError .validationError    let wp₂ ← wellTypedPolicy p₂ Γ |>.mapError .validationError    pure $ checkMatchesImplies wp₁ wp₂ (SymEnv.ofTypeEnv Γ)  ):= by  intro hwf  have h₁ := compile_ok_iff_welltypedpolicy_ok hwf (p := p₁)  have h₂ := compile_ok_iff_welltypedpolicy_ok hwf (p := p₂)  cases hcp₁ : CompiledPolicy.compile p₁ Γ  <;> cases hcp₂ : CompiledPolicy.compile p₂ Γ  <;> cases hwp₁ : wellTypedPolicy p₁ Γ  <;> cases hwp₂ : wellTypedPolicy p₂ Γ  -- this eliminates all the cases where the behavior of CompiledPolicy.compile is inconsistent  -- with the behavior of wellTypedPolicy on the same policy  <;> simp_all [Except.mapError, Except.isOk, Except.toBool]  case ok.ok.ok.ok cp₁ cp₂ wp₁ wp₂ =>    exact checkMatchesImpliesOpt_eqv_checkMatchesImplies_ok hwf hcp₁ hcp₂ hwp₁ hwp₂  case error.ok.error.ok | error.error.error.error =>    simp [CompiledPolicy.compile, Except.mapError, hwp₁] at hcp₁    simp [hcp₁]  case ok.error.ok.error =>    simp [CompiledPolicy.compile, Except.mapError, hwp₂] at hcp₂    simp [hcp₂]