let eq_rec =
(function a -> (function p -> (function a1 -> p)))
;;

let eq_rect =
(function a -> (function p -> (function a1 -> p)))
;;

let eq_rect' =
(function x -> (function p -> (function y -> p)))
;;

let eq_elim_r' =
(function x -> (function p -> (function y -> p)))
;;

let eq_elim_r'' =
(function x -> (function p -> (function y -> p)))
;;