yes, that is the actual construction: the disjunction data type only supports a lhs and rhs, so that is the only possible way to represent it. i wrote it the w

yes, that is the actual construction: the disjunction data type only supports a lhs and rhs, so that is the only possible way to represent it. i wrote it the way i did for clarity in the comments.