diff --git a/library/proof/Internal.scala b/library/proof/Internal.scala
index 3ac2903103998e0add424c95a8e213f23d94d5a4..72333c50108d266d01db29ff41f0db75c0359dde 100644
--- a/library/proof/Internal.scala
+++ b/library/proof/Internal.scala
@@ -2,8 +2,10 @@
 package leon.proof
 
 import leon.lang._
+import leon.annotation._
 
 /** Internal helper classes and methods for the 'proof' package. */
+@library
 object Internal {
 
   /*** Helper classes for relational reasoning ***/
diff --git a/library/proof/package.scala b/library/proof/package.scala
index fd07a8128439127a8c80b6f977a4f01d162415d9..f298dce2726e29394df38656e695824ed65661a6 100644
--- a/library/proof/package.scala
+++ b/library/proof/package.scala
@@ -9,6 +9,7 @@ import leon.proof.Internal._
 
 package object proof {
 
+  @library
   case class ProofOps(prop: Boolean) {
     def because(proof: Boolean): Boolean = proof && prop
     def neverHolds: Boolean = {
@@ -17,13 +18,17 @@ package object proof {
     }
   }
 
+  @library
   implicit def boolean2ProofOps(prop: Boolean): ProofOps = ProofOps(prop)
 
+  @library
   def trivial: Boolean = true
 
+  @library
   def by(proof: Boolean)(prop: Boolean): Boolean =
     proof && prop
 
+  @library
   def check(prop: Boolean): Boolean = {
     require(prop)
     prop
@@ -39,6 +44,7 @@ package object proof {
    *           x
    *         }.qed
    */
+  @library
   case class RelReasoning[A](x: A, prop: Boolean) {
 
     def ^^[B](r: (A, B) => Boolean): WithRel[A, B] = WithRel(x, r, prop)
@@ -52,6 +58,7 @@ package object proof {
     def qed: Boolean = prop
   }
 
+  @library
   implicit def any2RelReasoning[A](x: A): RelReasoning[A] =
     RelReasoning(x, true)