(* HIGHER ORDER REDUCIBILITY CANDIDATES ***************************************)
(* An arity is a type of λ→ to be used as carrier for a h.o. r.c. *)
(* HIGHER ORDER REDUCIBILITY CANDIDATES ***************************************)
(* An arity is a type of λ→ to be used as carrier for a h.o. r.c. *)