definition pr2 {A : Type} (a b : A) := a

check pr2
check pr2
check pr2
check @pr2
check @pr2
check @@pr2
check pr2