type (a :+: b) = (a, b)