diff --git a/core/Rule.ml b/core/Rule.ml
index 40bc823..97f0f28 100644
--- a/core/Rule.ml
+++ b/core/Rule.ml
@@ -1,10 +1,15 @@
+open Basis
 open Syntax
 open Effect
 
 type tp_rule = ltp L.m
-type chk_rule = gtp -> ltm L.m
 type syn_rule = gtm L.m
 
+type chk_rule =
+  | Chk of (gtp -> ltm L.m)
+  | BChk of (gtp -> ltm part -> ltm L.m)
+
+
 type tele_rule = (string list * ltele) L.m
 
 module TpRule =
@@ -17,8 +22,32 @@ end
 module ChkRule =
 struct
   type t = chk_rule
-  let rule x = x
-  let run x = x
+  let rule x = Chk x
+  let brule x = BChk x
+
+  let run =
+    function
+    | Chk x -> x
+    | BChk bchk ->
+      fun tp ->
+        bchk tp @@
+        Prt {supp = PBot; part = LAbort; env = Env.empty}
+
+  let brun =
+    let open Monad.Notation (L) in
+    function
+    | Chk chk ->
+      fun tp (Prt part) ->
+        let* ltm = chk tp in
+        let* () =
+          L.scope_thy (`Ext part.supp) @@
+          let* gtm = Eval.eval ltm in
+          let* gtm' = Eval.eval part.part in
+          Equate.equate_gtm tp gtm gtm'
+        in
+        L.ret ltm
+    | BChk bchk ->
+      bchk
 end
 
 module SynRule =
diff --git a/core/Rule.mli b/core/Rule.mli
index 798672e..179ffd1 100644
--- a/core/Rule.mli
+++ b/core/Rule.mli
@@ -15,7 +15,10 @@ end
 module ChkRule : sig
   type t = chk_rule
   val rule : (gtp -> ltm L.m) -> t
+  val brule : (gtp -> ltm part -> ltm L.m) -> t
+
   val run : t -> (gtp -> ltm L.m)
+  val brun : t -> (gtp -> ltm part -> ltm L.m)
 end
 
 module SynRule : sig