P x
     : Prop
R x x
     : Prop
fun (x : foo) (n : nat) => x n
     : foo -> nat -> nat
"1" 0
     : PAIR