--- /dev/null
+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)))
+;;
+