Always Matches Opt? eqv always Matches?

theorem alwaysMatchesOpt?_eqv_alwaysMatches? {p : Policy} {Γ : Validation.TypeEnv} :  Γ.WellFormed →  (do    let cp ← CompiledPolicy.compile p Γ    pure $ alwaysMatchesOpt? cp  ) =  (do    let wp ← wellTypedPolicy p Γ |>.mapError .validationError    pure $ alwaysMatches? wp (SymEnv.ofTypeEnv Γ)  ):= by  cases hcp : CompiledPolicy.compile p Γ  case ok cp =>    intro hwf    have ⟨wp, hwp, h⟩ := alwaysMatchesOpt?_eqv_alwaysMatches?_ok hwf hcp    simp [Except.mapError, hwp, h]  case error e =>    simp [Except.mapError]    cases hwp : wellTypedPolicy p Γ    case error e' =>      simp [CompiledPolicy.compile, Except.mapError, hwp] at hcp      simp [hcp]    case ok wp =>      intro hwf      have h := compile_ok_iff_welltypedpolicy_ok hwf (p := p)      simp [hcp, hwp, Except.isOk, Except.toBool] at h