f 1 0 (Rtrue (pr1 (pair 1 0)) 0) : nat