Action scope produces boolean

theorem action_scope_produces_boolean (policy : Policy) (request : Request) (entities : Entities) :  producesBool policy.actionScope.toExpr request entities:= by  simp only [producesBool, ActionScope.toExpr, Scope.toExpr, Bool.false_eq_true]  cases policy.actionScope  case actionInAny list =>    split    case h_1 => trivial    case h_2 res h =>      simp at h      have h₁ := action_in_set_of_euids_produces_boolean list request entities      unfold producesBool at h₁      split at h₁ <;> rename_i h₂      · simp [h₂] at h      · simp at h₁  case actionScope scope =>    simp only [Var.eqEntityUID, Var.inEntityUID, Var.isEntityType]    cases scope <;> simp [evaluate, apply₁, apply₂, Result.as]    case isMem ety uid =>      simp only [Coe.coe, Value.asBool, Except.bind_ok, beq_eq_false_iff_ne,        ne_eq, ite_not]      generalize (inₑ request.action uid entities) = b₁      generalize (ety == request.action.ty) = b₂      split <;> rename_i h      · trivial      · split at h <;> simp at h