diff --git a/library/shared/src/main/scala/org/sireum/contract.scala b/library/shared/src/main/scala/org/sireum/contract.scala
index 20f0ca7d..e48138f8 100644
--- a/library/shared/src/main/scala/org/sireum/contract.scala
+++ b/library/shared/src/main/scala/org/sireum/contract.scala
@@ -1670,6 +1670,7 @@ trait contract {
 
   implicit def $toB(state: Contract.StateCont): B = ???
 
+  implicit def $toSequent(b: Boolean): Contract.SequentBuilder = ???
   implicit def $toSequent(bs: (B, B)): Contract.SequentBuilder = ???
   implicit def $toSequent(bs: (B, B, B)): Contract.SequentBuilder = ???
   implicit def $toSequent(bs: (B, B, B, B)): Contract.SequentBuilder = ???
diff --git a/library/shared/src/main/scala/org/sireum/justification.scala b/library/shared/src/main/scala/org/sireum/justification.scala
index 102475d5..d5ba9e46 100644
--- a/library/shared/src/main/scala/org/sireum/justification.scala
+++ b/library/shared/src/main/scala/org/sireum/justification.scala
@@ -55,7 +55,7 @@ object justification {
 
   @just def Admit: Unit = $
 
-  @just def Rewrite(rs: RS): Unit = $
+  @just def Rewrite(rs: RS, from: StepId): Unit = $
 
   object natded {