diff --git a/library/lang/Rational.scala b/library/lang/Rational.scala
index c8027dee9c801e3d59505e4a307ca21d901fedba..f4a10215b61032a73f20107c5aeddbac841e66bc 100644
--- a/library/lang/Rational.scala
+++ b/library/lang/Rational.scala
@@ -82,6 +82,7 @@ case class Rational(numerator: BigInt, denominator: BigInt) {
   }
 }
 
+@library
 object Rational {
 
   implicit def bigIntToRat(n: BigInt): Rational = Rational(n, 1)
diff --git a/library/proof/Internal.scala b/library/proof/Internal.scala
index 72333c50108d266d01db29ff41f0db75c0359dde..ad395f5326884a34be16eda85a84e01f5bf323d8 100644
--- a/library/proof/Internal.scala
+++ b/library/proof/Internal.scala
@@ -5,11 +5,10 @@ import leon.lang._
 import leon.annotation._
 
 /** Internal helper classes and methods for the 'proof' package. */
-@library
 object Internal {
 
   /*** Helper classes for relational reasoning ***/
-
+  @library
   case class WithRel[A, B](x: A, r: (A, B) => Boolean, prop: Boolean) {
 
     /** Continue with the next relation. */
@@ -33,6 +32,7 @@ object Internal {
     def qed: Boolean = prop
   }
 
+  @library
   case class WithProof[A, B](
     x: A, r: (A, B) => Boolean, proof: Boolean, prop: Boolean) {