1 2 3 4 5
Notation prop_fun x y := (fun (x : Prop) => y). Definition foo := fun (p : Prop) => p. Definition bar := fun (_ : Prop) => O. Print foo. Print bar.