diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index aaf3054ae57bcad27a322003311fad84d208ce03..85d20e1d7732e2d302517c0790bac2d94fa8ec8d 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -9,7 +9,8 @@ import rules._
 object Rules {
   def all = Set[Synthesizer => Rule](
     new Unification.DecompTrivialClash(_),
-    new Unification.OccursCheck(_),
+    new Unification.OccursCheck(_), // probably useless
+    new Disunification.Decomp(_),
     new ADTDual(_),
     new OnePoint(_),
     new Ground(_),
diff --git a/src/main/scala/leon/synthesis/rules/Disunification.scala b/src/main/scala/leon/synthesis/rules/Disunification.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9cf574acfaf7dda15898b436e61dcfb065a0c8d3
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -0,0 +1,36 @@
+package leon
+package synthesis
+package rules
+
+import purescala.Trees._
+import purescala.TypeTrees._
+import purescala.TreeOps._
+import purescala.Extractors._
+
+object Disunification {
+  class Decomp(synth: Synthesizer) extends Rule("Disunif. Decomp.", synth, 200) {
+    def attemptToApplyOn(p: Problem): RuleResult = {
+      val TopLevelAnds(exprs) = p.phi
+
+      val (toRemove, toAdd) = exprs.collect {
+        case neq @ Not(Equals(cc1 @ CaseClass(cd1, args1), cc2 @ CaseClass(cd2, args2))) =>
+          if (cc1 == cc2) {
+            (neq, List(BooleanLiteral(false)))
+          } else if (cd1 == cd2) {
+            (neq, (args1 zip args2).map(p => Not(Equals(p._1, p._2))))
+          } else {
+            (neq, List(BooleanLiteral(true)))
+          }
+      }.unzip
+
+      if (!toRemove.isEmpty) {
+        val sub = p.copy(phi = Or((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
+
+        RuleFastStep(List(sub), forward)
+      } else {
+        RuleInapplicable
+      }
+    }
+  }
+}
+
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index f7aec99598eeef15b2caf31a6ae17abb3b0922d1..5315eee035d3ea266bd38c231b4282b65b0cac80 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -34,6 +34,8 @@ object Unification {
     }
   }
 
+  // This rule is probably useless; it never happens except in crafted
+  // examples, and will be found by OptimisticGround anyway.
   class OccursCheck(synth: Synthesizer) extends Rule("Unif OccursCheck", synth, 200) {
     def attemptToApplyOn(p: Problem): RuleResult = {
       val TopLevelAnds(exprs) = p.phi