diff --git a/src/funcheck/scalacheck/ScalaCheck.scala b/src/funcheck/scalacheck/ScalaCheck.scala
index 17fa79e311da8ee43a9a9867d161bf446a8883fe..3251de8db4d29772cd4bdc94a80bf4253d5c58f2 100644
--- a/src/funcheck/scalacheck/ScalaCheck.scala
+++ b/src/funcheck/scalacheck/ScalaCheck.scala
@@ -9,28 +9,42 @@ import funcheck.util.FreshNameCreator
  */
 trait ScalaCheck extends FreshNameCreator {
   val global: Global
-  
   import global._
   
+    /** Transform the string <code>name</code> in method symbols from the <code>sym</code> 
+     * class symbol. */
+    private def symDecl(sym: Symbol, name: String) = sym.tpe.decl(name)
+  
+    /** Retrieve the constructor Symbol for the passed <code>cs</code> class symbol. */
+    private def constructorDecl(cs: ClassSymbol) = cs.tpe.decl(nme.CONSTRUCTOR)
   
-  /** Transform string name in method symbols from the <code>symDecl</code> 
-    * class symbol. */
-  private def symDecl(sym: Symbol, name: String) = sym.tpe.decl(name)
+  trait GenericScalaCheckModule {
+    protected val moduleSym: Symbol
+    protected lazy val classSym = moduleSym.linkedClassOfModule
+  
+    
+    protected def modDecl(method: String) = symDecl(moduleSym, method)
+    protected def classDecl(method: String) = symDecl(classSym, method)
+    
+  
+    protected def select(instance: Symbol, method: String): Select = 
+      Select(Ident(instance), symDecl(instance,method))
+    
+    protected def apply(lhs: Tree, rhs: Tree): Apply = 
+      apply(lhs, List(rhs))
+    
+    protected def apply(lhs: Tree, rhs: List[Tree]): Apply = 
+      Apply(lhs, rhs)
+  }
   
-  /** Retrieve the constructor Symbol for the passed <code>cs</code> class symbol. */
-  private def constructorDecl(cs: ClassSymbol) = cs.tpe.decl(nme.CONSTRUCTOR)
   
   /** Module for creating scalac Tree nodes for calling methods of the 
    * <code>org.scalacheck.Gen</code> class and module.*/
-  object Gen {
+  object Gen extends GenericScalaCheckModule {
   
     /** Symbol for the <code>org.scalacheck.Gen</code> module definition. */
-    private lazy val moduleGenSym = definitions.getModule("org.scalacheck.Gen")
+    override protected lazy val moduleSym = definitions.getModule("org.scalacheck.Gen")
     
-    /** Symbol for the <code>org.scalacheck.Gen</code> class definition. */
-    private lazy val classGenSym = moduleGenSym.linkedClassOfModule                  
-  
-  
     /**
      * Apply <code>polyTpe</code> to the polymorphic type <code>org.scalacheck.Gen</code>.
      * 
@@ -39,7 +53,7 @@ trait ScalaCheck extends FreshNameCreator {
      *         to the polymorphic type <code>org.scalacheck.Gen</code>, i.e., 
      *         <code>Gen[polyTpe]</code>.
      */
-    private def applyType(polyTpe: Type) = appliedType(classGenSym.tpe, List(polyTpe))
+    private def applyType(polyTpe: Type) = appliedType(classSym.tpe, List(polyTpe))
     
     
     /**
@@ -48,8 +62,7 @@ trait ScalaCheck extends FreshNameCreator {
      * typer phase (this usually means that the typer has to be called explictly, 
      * so it is the developer duty to ensure that this happen at some point).
      */
-    def value(rhs: Tree): Tree =
-      Apply(Select(Ident(moduleGenSym), symDecl(moduleGenSym, "value")), List(rhs))
+    def value(rhs: Tree): Tree = apply(select(moduleSym, "value"), rhs)
     
     
     /**
@@ -59,10 +72,10 @@ trait ScalaCheck extends FreshNameCreator {
      * so it is the developer duty to ensure that this happen at some point).
      */
     def oneOf(generators: List[Symbol]): Tree = 
-      Apply(Select(Ident(moduleGenSym), symDecl(moduleGenSym, "oneOf")), generators.map(Ident(_)))
+      apply(select(moduleSym, "oneOf"), generators.map(Ident(_)))
     
-    def lzy(generator: Tree): Tree = 
-      Apply(Select(Ident(moduleGenSym), symDecl(moduleGenSym, "lzy")), List(generator))
+    
+    def lzy(generator: Tree): Tree = apply(select(moduleSym, "lzy"), generator)
     
     /**
      * This creates a Tree node for the call <code>org.scalacheck.Gen.flatMap[T](body)</code>, 
@@ -71,7 +84,7 @@ trait ScalaCheck extends FreshNameCreator {
      * so it is the developer duty to ensure that this happen at some point).
      */
     def flatMap(qualifier: Tree, body: Tree): Tree = 
-      Apply(Select(qualifier, symDecl(classGenSym, "flatMap")),List(body))
+      apply(Select(qualifier, classDecl("flatMap")), body)
      
     
     /**
@@ -81,7 +94,7 @@ trait ScalaCheck extends FreshNameCreator {
      * so it is the developer duty to ensure that this happen at some point).
      */
     def map(qualifier: Tree, body: Tree): Tree = 
-      Apply(Select(qualifier, symDecl(classGenSym, "map")), List(body))
+      apply(Select(qualifier, classDecl("map")), body)
      
     
     
@@ -270,50 +283,36 @@ trait ScalaCheck extends FreshNameCreator {
   
   /** Module for creating scalac Tree nodes for calling methods of the 
    * <code>org.scalacheck.Arbitrary</code> class and module.*/
-  object Arbitrary {
-   
-    /** Symbol for the <code>org.scalacheck.Arbitrary</code> module definition. */
-    private val moduleArbitrarySym = definitions.getModule("org.scalacheck.Arbitrary")
+  object Arbitrary extends GenericScalaCheckModule {
     
-    /** Symbol for the <code>org.scalacheck.Arbitrary</code> class definition. */
-    private val classArbitrarySym = moduleArbitrarySym.linkedClassOfModule 
     
+    /** Symbol for the <code>org.scalacheck.Arbitrary</code> module definition. */
+    override protected lazy val moduleSym = definitions.getModule("org.scalacheck.Arbitrary")
     
     /** Symbol for the <code>org.scalacheck.Arbitrary.arbInt</code> method definition. */
-    private val arbInt          =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbInt"))
-    
+    private val arbInt          =  select(moduleSym, "arbInt")
     /** Symbol for the <code>org.scalacheck.Arbitrary.arbBool</code> method definition. */
-    private val arbBool         =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbBool"))
-    
+    private val arbBool         =  select(moduleSym, "arbBool")
     /** Symbol for the <code>org.scalacheck.Arbitrary.arbLong</code> method definition. */
-    private val arbLong         =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbLong"))
-    
+    private val arbLong         =  select(moduleSym, "arbLong")
     /** Symbol for the <code>org.scalacheck.Arbitrary.arbThrowable</code> method definition. */
-    private val arbThrowable    =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbThrowable"))
-    
+    private val arbThrowable    =  select(moduleSym, "arbThrowable")
     /** Symbol for the <code>org.scalacheck.Arbitrary.arbDouble</code> method definition. */
-    private val arbDouble       =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbDouble"))
-    
+    private val arbDouble       =  select(moduleSym, "arbDouble")
     /** Symbol for the <code>org.scalacheck.Arbitrary.arbChar</code> method definition. */
-    private val arbChar         =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbChar"))
-    
+    private val arbChar         =  select(moduleSym, "arbChar")
     /** Symbol for the <code>org.scalacheck.Arbitrary.arbString</code> method definition. */
-    private val arbString       =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbString"))
-    
+    private val arbString       =  select(moduleSym, "arbString")
     /** Symbol for the <code>org.scalacheck.Arbitrary.arbOption</code> method definition. */
-    private val arbOption       =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbOption"))
-    
+    private val arbOption       =  select(moduleSym, "arbOption")
     /** Symbol for the <code>org.scalacheck.Arbitrary.arbImmutableMap</code> method definition. */
-    private val arbImmutableMap =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbImmutableMap"))
-    
+    private val arbImmutableMap =  select(moduleSym, "arbImmutableMap")
     /** Symbol for the <code>org.scalacheck.Arbitrary.arbList</code> method definition. */
-    private val arbList         =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbList"))
-    
+    private val arbList         =  select(moduleSym, "arbList")
     /** Symbol for the <code>org.scalacheck.Arbitrary.arbSet</code> method definition. */
-    private val arbSet          =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbSet"))
-    
+    private val arbSet          =  select(moduleSym, "arbSet")
     /** Symbol for the <code>org.scalacheck.Arbitrary.arbTuple2</code> method definition. */
-    private val arbTuple2       =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbTuple2"))
+    private val arbTuple2       =  select(moduleSym, "arbTuple2")
     
     //[[TODO]]
     //lazy val arbMultiSet       =  Select(Ident(arbitraryModule), arbitraryModule.tpe.decl("arbMultiSet"))
@@ -323,14 +322,25 @@ trait ScalaCheck extends FreshNameCreator {
     /** Map that stores <code>org.scalacheck.Arbitrary.arbitrary[Type]</code> calls. */
     protected val tpe2arbApp    = scala.collection.mutable.Map.empty[Type,Tree]
     
+    
     // initialize map with ScalaCheck built-in types that are part of our PureScala language
-    tpe2arbApp += definitions.IntClass.typeConstructor       -> arbInt
-    tpe2arbApp += definitions.BooleanClass.typeConstructor   -> arbBool
-    tpe2arbApp += definitions.LongClass.typeConstructor      -> arbLong
-    tpe2arbApp += definitions.ThrowableClass.typeConstructor -> arbThrowable
-    tpe2arbApp += definitions.DoubleClass.typeConstructor    -> arbDouble
-    tpe2arbApp += definitions.CharClass.typeConstructor      -> arbChar
-    tpe2arbApp += definitions.StringClass.typeConstructor    -> arbString
+    import definitions._
+    tpe2arbApp += IntClass.typeConstructor       -> arbInt
+    tpe2arbApp += BooleanClass.typeConstructor   -> arbBool
+    tpe2arbApp += LongClass.typeConstructor      -> arbLong
+    tpe2arbApp += ThrowableClass.typeConstructor -> arbThrowable
+    tpe2arbApp += DoubleClass.typeConstructor    -> arbDouble
+    tpe2arbApp += CharClass.typeConstructor      -> arbChar
+    tpe2arbApp += StringClass.typeConstructor    -> arbString
+    tpe2arbApp += OptionClass.typeConstructor    -> arbOption
+    
+    lazy val ImmutableMapClass: Symbol = getClass("scala.collection.immutable.Map")
+    lazy val ImmutableSetClass: Symbol = getClass("scala.collection.immutable.Set")
+    
+    tpe2arbApp += ImmutableMapClass.typeConstructor    -> arbImmutableMap
+    tpe2arbApp += ListClass.typeConstructor            -> arbList
+    tpe2arbApp += ImmutableSetClass.typeConstructor    -> arbSet
+    tpe2arbApp += TupleClass(2).typeConstructor        -> arbTuple2 
     
     /**
      * Apply <code>polyTpe</code> to the polymorphic type <code>org.scalacheck.Arbitrary</code>.
@@ -340,7 +350,7 @@ trait ScalaCheck extends FreshNameCreator {
      *         to the polymorphic type <code>org.scalacheck.Arbitrary</code>, i.e., 
      *         <code>Arbitrary[polyTpe]</code>.
      */
-    private def applyType(tpe: Type) = appliedType(classArbitrarySym.tpe, List(tpe))
+    private def applyType(tpe: Type) = appliedType(classSym.tpe, List(tpe))
     
     /**
      * Creates a Tree node for the call <code>org.scalacheck.Arbitrary.apply[T](generator)</code>, 
@@ -348,10 +358,13 @@ trait ScalaCheck extends FreshNameCreator {
      * typer phase (this usually means that the typer has to be called explictly, 
      * so it is the developer duty to ensure that this happen at some point).
      */
-    def apply(generator: Tree): Tree = 
-      Apply(Select(Ident(moduleArbitrarySym),symDecl(moduleArbitrarySym, "apply")), List(generator))
+    def apply(generator: Tree): Tree = apply(select(moduleSym, "apply"), generator)
     
-    def arbitrary(tpe: Type): Tree = tpe2arbApp.get(tpe).get
+    def arbitrary(tpe: Type): Tree = tpe match {
+      //case TypeRef(_,sym,List(p)) if p.prefix == NoPrefix => tpe2arbApp.get(tpe).get
+      case TypeRef(_,sym,List(p)) => apply(arbitrary(sym.typeConstructor), arbitrary(p))
+      case tpe => tpe2arbApp.get(tpe).get
+    }
     
     /**
      * 
@@ -394,8 +407,8 @@ trait ScalaCheck extends FreshNameCreator {
     }
     
                                   
-    protected def applyArbitrary(param: Tree): Apply =
-      Apply(Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbitrary")), List(param))
+    protected def applyArbitrary(param: Tree): Apply = 
+      apply(select(moduleSym, "arbitrary"), param)
     
     
     /**
@@ -437,9 +450,9 @@ trait ScalaCheck extends FreshNameCreator {
     
     def forAll(prop: Tree): Apply = forAll(List(prop))
     
+    def ==>(ifz: Tree, then: Tree): Apply = moduleApply("==>", List(ifz,propBoolean(then)))
     
-    def propBoolean(ident: Tree): Apply = 
-      moduleApply("propBoolean", List(ident))
+    def propBoolean(prop: Tree): Apply = moduleApply("propBoolean", List(prop))
   }