How to use the mythril.laser.smt.bool.Bool function in mythril

def _comparison_helper(
    a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool
) -> Bool:
    annotations = a.annotations.union(b.annotations)
    if isinstance(a, BitVecFunc):
        return _func_comparison_helper(a, b, operation, default_value, inputs_equal)
    return Bool(operation(a.raw, b.raw), annotations)

def Or(*args: Union[Bool, bool]) -> Bool:
    """Create an or expression.

    :param a:
    :param b:
    :return:
    """
    args_list = [arg if isinstance(arg, Bool) else Bool(arg) for arg in args]
    union = [arg.annotations for arg in args_list]
    return Bool(z3.Or([a.raw for a in args_list]), annotations=union)

else:
            condition = z3.And(
                condition,
                z3.Or(
                    z3.Not((a_nest.input_ != b_nest.input_).raw),
                    (a_nest.raw == b_nest.raw),
                ),
                z3.Or(
                    z3.Not((a_nest.raw == b_nest.raw)),
                    (a_nest.input_ != b_nest.input_).raw,
                ),
            )

    comparision = And(
        Bool(cast(z3.BoolRef, operation(a.raw, b.raw)), annotations=union),
        Bool(condition) if b.nested_functions else Bool(True),
        a.input_ == b.input_ if inputs_equal else a.input_ != b.input_,
    )
    if a.potential_values:
        for i, val in enumerate(a.potential_values):
            comparision = Or(comparision, And(operation(val[0].raw, b.raw), val[1]))

    comparision.simplify()
    return comparision

condition = False
            for value, cond in a.potential_values:
                if value is not None:
                    condition = Or(condition, And(operation(b.raw, value.value), cond))
            ret = And(condition, operation(a.raw, b.raw), paddded_cond)
            return ret

        return And(operation(a.raw, b.raw), paddded_cond)
    if (
        not isinstance(b, BitVecFunc)
        or not a.func_name
        or not a.input_
        or not a.func_name == b.func_name
        or str(operation) not in ("", "")
    ):
        return Bool(z3.BoolVal(default_value), annotations=union)

    condition = True
    for a_nest, b_nest in product(a.nested_functions, b.nested_functions):
        if a_nest.func_name != b_nest.func_name:
            continue
        if a_nest.func_name == "Hybrid":
            continue
        # a.input (eq/neq) b.input ==> a == b
        if inputs_equal:
            condition = z3.And(
                condition,
                z3.Or(
                    z3.Not((a_nest.input_ == b_nest.input_).raw),
                    (a_nest.raw == b_nest.raw),
                ),
                z3.Or(

def BVSubNoUnderflow(
    a: Union[BitVec, int], b: Union[BitVec, int], signed: bool
) -> Bool:
    """Creates predicate that verifies that the subtraction doesn't overflow.

    :param a:
    :param b:
    :param signed:
    :return:
    """
    if not isinstance(a, BitVec):
        a = BitVec(z3.BitVecVal(a, 256))
    if not isinstance(b, BitVec):
        b = BitVec(z3.BitVecVal(b, 256))

    return Bool(z3.BVSubNoUnderflow(a.raw, b.raw, signed))

def BVAddNoOverflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool) -> Bool:
    """Creates predicate that verifies that the addition doesn't overflow.

    :param a:
    :param b:
    :param signed:
    :return:
    """
    if not isinstance(a, BitVec):
        a = BitVec(z3.BitVecVal(a, 256))
    if not isinstance(b, BitVec):
        b = BitVec(z3.BitVecVal(b, 256))
    return Bool(z3.BVAddNoOverflow(a.raw, b.raw, signed))

def And(*args: Union[Bool, bool]) -> Bool:
    """Create an And expression."""
    union = []
    args_list = [arg if isinstance(arg, Bool) else Bool(arg) for arg in args]
    for arg in args_list:
        union.append(arg.annotations)
    return Bool(z3.And([a.raw for a in args_list]), union)

def __eq__(self, other: Union[int, "BitVec"]) -> Bool:  # type: ignore
        """Create an equality expression.

        :param other:
        :return:
        """
        if not isinstance(other, BitVec):
            return Bool(
                cast(z3.BoolRef, self.raw == other), annotations=self.annotations
            )

        union = self.annotations.union(other.annotations)
        # Some of the BitVecs can be 512 bit due to sha3()
        eq_check = _padded_operation(self.raw, other.raw, eq)
        # MYPY: fix complaints due to z3 overriding __eq__
        return Bool(cast(z3.BoolRef, eq_check), annotations=union)