left(■) : Unit + Nat \(x:Void). 3