Check Implies Opt eqv check Implies

theorem checkImpliesOpt_eqv_checkImplies {ps₁ ps₂ : Policies} {Γ : Validation.TypeEnv} :  Γ.WellFormed →  (do    let cpset₁ ← CompiledPolicySet.compile ps₁ Γ    let cpset₂ ← CompiledPolicySet.compile ps₂ Γ    pure $ checkImpliesOpt cpset₁ cpset₂  ) =  (do    let wps₁ ← wellTypedPolicies ps₁ Γ |>.mapError .validationError    let wps₂ ← wellTypedPolicies ps₂ Γ |>.mapError .validationError    pure $ checkImplies wps₁ wps₂ (SymEnv.ofTypeEnv Γ)  ):= by  intro hwf  have h₁ := compile_ok_iff_welltypedpolicies_ok hwf (ps := ps₁)  have h₂ := compile_ok_iff_welltypedpolicies_ok hwf (ps := ps₂)  cases hcpset₁ : CompiledPolicySet.compile ps₁ Γ  <;> cases hcpset₂ : CompiledPolicySet.compile ps₂ Γ  <;> cases hwps₁ : wellTypedPolicies ps₁ Γ  <;> cases hwps₂ : wellTypedPolicies ps₂ Γ  -- this eliminates all the cases where the behavior of CompiledPolicySet.compile is inconsistent  -- with the behavior of wellTypedPolicies on the same policyset  <;> simp_all [Except.mapError, Except.isOk, Except.toBool]  case ok.ok.ok.ok cpset₁ cpset₂ wps₁ wps₂ =>    have ⟨wps₁', wps₂', hwps₁', hwps₂', h⟩ := checkImpliesOpt_eqv_checkImplies_ok hwf hcpset₁ hcpset₂    simp_all  case error.ok.error.ok | error.error.error.error =>    simp [CompiledPolicySet.compile, Except.mapError, hwps₁] at hcpset₁    simp [hcpset₁]  case ok.error.ok.error =>    simp [CompiledPolicySet.compile, Except.mapError, hwps₂] at hcpset₂    simp [hcpset₂]