<SYSTEM_TASK:>
Solve the following problem using Python, implementing the functions described below, one line at a time
<END_TASK>
<USER_TASK:>
Description:
 def Or(a: Bool, b: Bool) -> Bool: """Create an or expression. :param a: :param b: :return: """

    union = a.annotations + b.annotations
    return Bool(z3.Or(a.raw, b.raw), annotations=union)