+let message1 st1 m t1 =
+ L.et_items1 "In the environment" m st1 t1
+
+let log1 s m t =
+ let s = s ^ " the term" in
+ L.log R.specs level (message1 s m t)
+
+let error1 err s m t =
+ err (message1 s m t)
+
+let message3 m t1 t2 ?mu t3 =
+ let sm, st1, st2 = "In the environment", "the term", "is of type" in
+ match mu with
+ | Some mu ->
+ let smu, st3 = "but in the environment", "it must be of type" in
+ L.et_items3 sm m st1 t1 st2 t2 ~sc3:smu ~c3:mu st3 t3
+ | None ->
+ let st3 = "but it must be of type" in
+ L.et_items3 sm m st1 t1 st2 t2 st3 t3
+
+let error3 err m t1 t2 ?mu t3 =
+ err (message3 m t1 t2 ?mu t3)
+
+let assert_convertibility err f st m u w v =
+ if R.are_convertible st m u m w then f () else
+ error3 err m v w u
+
+let assert_applicability err f st m u w v =
+ match R.xwhd st m u with
+ | _, B.Sort _ -> error1 err "not a function type" m u
+ | mu, B.Bind (_, B.Abst u, _) ->
+ if R.are_convertible st mu u m w then f () else
+ error3 err m v w ~mu u
+ | _ -> assert false (**)