module LowerPatVar import Prelude foo : Nat × Nat → Nat foo (ZZ , y) = Z