def f : Unit → Nat :=
fun a => 10
def g : Unit → Unit :=
fun a =>
  match a with
  | b@h:PUnit.unit => b