Verify Equivalent is ok and sound

theorem verifyEquivalent_is_ok_and_sound {ps₁ ps₁' ps₂ ps₂' : Policies} {Γ : TypeEnv} :  Γ.WellFormed →  wellTypedPolicies ps₁ Γ = .ok ps₁' →  wellTypedPolicies ps₂ Γ = .ok ps₂' →  ∃ asserts,    verifyEquivalent ps₁' ps₂' (SymEnv.ofEnv Γ) = .ok asserts ∧    (SymEnv.ofEnv Γ ⊭ asserts →      ∀ env : Env,        InstanceOfWellFormedEnvironment env.request env.entities Γ →        env.StronglyWellFormedForPolicies ps₁' →        env.StronglyWellFormedForPolicies ps₂' →        bothAllowOrBothDeny          (Spec.isAuthorized env.request env.entities ps₁)          (Spec.isAuthorized env.request env.entities ps₂)):= by  intros hwf hwt₁ hwt₂  have hwf_εnv₁ := ofEnv_swf_for_policies hwf hwt₁  have hwf_εnv₂ := ofEnv_swf_for_policies hwf hwt₂  have ⟨asserts, hok⟩ := verifyEquivalent_is_ok hwf hwt₁ hwt₂  exists asserts  simp only [hok, true_and]  intros hunsat env hinst hwf_ps₁ hwf_ps₂  simp only [    wellTypedPolicies_preserves_isAuthorized hinst hwt₁,    wellTypedPolicies_preserves_isAuthorized hinst hwt₂,  ]  apply verifyEquivalent_is_sound hwf_εnv₁ hwf_εnv₂ hok hunsat env _ hwf_ps₁ hwf_ps₂  exact ofEnv_soundness hwf_ps₁.1 hinst