let rec aux (k, n) j = match n.v with
| Fin i when i = j -> true
| Fin i ->
Printf.printf "binder %s is %u but must be %u\n" (P.string_of_mark k) i j; true (**)
| Inf ->
Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; true (**)
let rec aux (k, n) j = match n.v with
| Fin i when i = j -> true
| Fin i ->
Printf.printf "binder %s is %u but must be %u\n" (P.string_of_mark k) i j; true (**)
| Inf ->
Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; true (**)