Verify Always Matches is ok and sound

theorem verifyAlwaysMatches_is_ok_and_sound {p p' : Policy} {Γ : TypeEnv} :  Γ.WellFormed →  wellTypedPolicy p Γ = .ok p' →  ∃ asserts,    verifyAlwaysMatches p' (SymEnv.ofEnv Γ) = .ok asserts ∧    (SymEnv.ofEnv Γ ⊭ asserts →      ∀ env : Env,        InstanceOfWellFormedEnvironment env.request env.entities Γ →        env.StronglyWellFormedForPolicy p' →        evaluate p.toExpr env.request env.entities = .ok (.prim (.bool true))):= by  intros hwf hwt  have hwf_εnv := ofEnv_swf_for_policy hwf hwt  have ⟨asserts, hok⟩ := verifyAlwaysMatches_is_ok hwf hwt  exists asserts  simp only [hok, true_and]  intros hunsat env hinst hwf_env  simp only [wellTypedPolicy_preserves_evaluation hinst hwt]  have := verifyEvaluate_is_sound verifyAlwaysMatches_wbeq hwf_εnv hok hunsat env  simp [beq_iff_eq] at this  apply this _ hwf_env  exact ofEnv_soundness hwf_env.1 hinst