bv_decide
x : Bool
x✝ : x = true
⊢ (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
      (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))) =
    true
no goals