Verify Implies is ok and complete

theorem verifyImplies_is_ok_and_complete {ps₁ ps₁' ps₂ ps₂' : Policies} {Γ : TypeEnv} :  Γ.WellFormed →  wellTypedPolicies ps₁ Γ = .ok ps₁' →  wellTypedPolicies ps₂ Γ = .ok ps₂' →  ∃ asserts,    verifyImplies ps₁' ps₂' (SymEnv.ofEnv Γ) = .ok asserts ∧    (SymEnv.ofEnv Γ ⊧ asserts →      ∃ env : Env,        InstanceOfWellFormedEnvironment env.request env.entities Γ ∧        env.StronglyWellFormedForPolicies ps₁' ∧        env.StronglyWellFormedForPolicies ps₂' ∧        ¬ ifFirstAllowsSoDoesSecond          (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⟩ := verifyImplies_is_ok hwf hwt₁ hwt₂  exists asserts  simp only [hok, true_and]  intros hsat  have ⟨env, hmodel, hswf_env₁, hswf_env₂, henum_comp, hres⟩ := verifyImplies_is_complete hwf_εnv₁ hwf_εnv₂ hok hsat  have hinst := ofEnv_completeness hwf hswf_env₁.1 henum_comp hmodel  simp only [    ←wellTypedPolicies_preserves_isAuthorized hinst hwt₁,    ←wellTypedPolicies_preserves_isAuthorized hinst hwt₂,  ] at hres  exists env