def f1 : Nat × Bool → Nat
  | _ => 0

def f2 : (α : Type) × α × α → Nat
  | _ => 0

def f3 : (x : Nat) × Bool → Nat
  | _ => 0