Verify Always Allows is complete

theorem verifyAlwaysAllows_is_complete {ps₁ : Policies} {εnv : SymEnv} {asserts : Asserts} :  εnv.StronglyWellFormedForPolicies ps₁ →  verifyAlwaysAllows ps₁ εnv = .ok asserts →  εnv ⊧ asserts →  ∃ env,    env ∈ᵢ εnv ∧    env.StronglyWellFormedForPolicies ps₁ ∧    Env.EnumCompleteFor env εnv ∧    ¬ allows (Spec.isAuthorized env.request env.entities ps₁):= by  intro hwε₁ hvc hsat  unfold verifyAlwaysAllows at hvc  have ⟨env, h⟩ := verifyIsAuthorized_is_complete verifyImplies_wbaq    (swf_εnv_for_allowAll_policies hwε₁.left) hwε₁ hvc hsat  exists env  rw [allows_eq_allowAll_implies _ env]  simp [h]