∀ {x y : Std.Tactic.BVDecide.BVLogicalExpr} {assign : Std.Tactic.BVDecide.BVExpr.Assignment},
  x.Sat assign →
    y.Sat assign →
      Std.Tactic.BVDecide.BVLogicalExpr.Sat (Std.Tactic.BVDecide.BoolExpr.gate Std.Tactic.BVDecide.Gate.and x y) assign