Implies Opt? eqv implies? ok

theorem impliesOpt?_eqv_implies?_ok {ps₁ ps₂ : Policies} {cpset₁ cpset₂ : CompiledPolicySet} {Γ : Validation.TypeEnv} :  Γ.WellFormed →  CompiledPolicySet.compile ps₁ Γ = .ok cpset₁ →  CompiledPolicySet.compile ps₂ Γ = .ok cpset₂ →  ∃ wps₁ wps₂,    wellTypedPolicies ps₁ Γ = .ok wps₁ ∧    wellTypedPolicies ps₂ Γ = .ok wps₂ ∧    impliesOpt? cpset₁ cpset₂ = implies? wps₁ wps₂ (SymEnv.ofTypeEnv Γ):= by  simp [implies?, impliesOpt?]  simp [sat?]  intro hwf hcpset₁ hcpset₂  have ⟨wps₁, hwps₁⟩ := compile_ok_then_exists_wtps hwf hcpset₁  exists wps₁ ; apply And.intro hwps₁  have ⟨wps₂, hwps₂⟩ := compile_ok_then_exists_wtps hwf hcpset₂  exists wps₂ ; apply And.intro hwps₂  have ⟨asserts, h₁⟩ := verifyImplies_is_ok hwf hwps₁ hwps₂  simp [h₁]  have := cpset_satAssertsOpt?_eqv_satAsserts?_ok (pss := [ps₁, ps₂]) (wpss := [wps₁, wps₂]) (cpsets := [cpset₁, cpset₂]) (asserts := asserts) (Γ := Γ) (by simp) (by simp)  simp only [List.flatten_cons, List.flatten_nil, List.append_nil, List.map_cons, List.map_nil] at this  rw [this] ; clear this  · have := verifyImpliesOpt_eqv_verifyImplies_ok hcpset₁ hcpset₂ hwps₁ hwps₂    simp [h₁, ResultAssertsEquiv] at this    exact Asserts.Equiv.satAssertsOpt? [.pset cpset₁, .pset cpset₂] (Asserts.Equiv.symm this)  · simp [hcpset₁, hcpset₂]  · simp [hwps₁, hwps₂]