And produces bool or error

theorem and_produces_bool_or_error (e₁ e₂ : Expr) (request : Request) (entities : Entities) :  match (evaluate (Expr.and e₁ e₂) request entities) with  | .ok (.prim (.bool _)) => true  | .error _ => true  | _ => false:= by  cases h : evaluate (Expr.and e₁ e₂) request entities <;> simp  case ok val =>    cases val    <;> simp only [evaluate, Result.as, Coe.coe, Value.asBool, Bool.not_eq_true', pure, Except.pure] at h    <;> generalize (evaluate e₁ request entities) = r₁ at h    <;> generalize (evaluate e₂ request entities) = r₂ at h    case prim prim =>      cases prim <;> simp      case int | string | entityUID =>        split at h <;> split at h <;> simp only [Except.bind_ok, Except.bind_err, reduceCtorEq] at h        split at h        case _ => simp only [Except.ok.injEq, Value.prim.injEq, reduceCtorEq] at h        case _ =>          split at h          case _ => split at h <;> simp only [Except.bind_ok, Except.bind_err, Except.ok.injEq, Value.prim.injEq, reduceCtorEq] at h          case _ => simp only [Except.bind_err, reduceCtorEq] at h    case set | record | ext =>      exfalso      split at h <;> split at h <;> simp only [Except.bind_ok, Except.bind_err, reduceCtorEq] at h      split at h      · simp only [Except.ok.injEq, reduceCtorEq] at h      · split at h        · split at h <;> simp only [Except.bind_ok, Except.bind_err, Except.ok.injEq, reduceCtorEq] at h        · simp only [Except.bind_err, reduceCtorEq] at h