diff --git a/src/lower/mod.rs b/src/lower/mod.rs
index 5049d705668..13254f3c1cc 100644
--- a/src/lower/mod.rs
+++ b/src/lower/mod.rs
@@ -1018,6 +1018,68 @@ impl Anonymize for [ir::ParameterKind<ir::Identifier>] {
     }
 }
 
+trait ExpandWhereClauses {
+    fn expanded_where_clauses(&self, program: &ir::Program) -> Vec<ir::DomainGoal>;
+}
+
+impl ExpandWhereClauses for ir::StructDatumBound {
+    fn expanded_where_clauses(&self, program: &ir::Program) -> Vec<ir::DomainGoal> {
+        self.where_clauses
+            .iter()
+            .cloned()
+            .flat_map(|wc| wc.expanded(program))
+            .collect()
+    }
+}
+
+impl ExpandWhereClauses for ir::TraitDatumBound {
+    fn expanded_where_clauses(&self, program: &ir::Program) -> Vec<ir::DomainGoal> {
+        self.where_clauses
+            .iter()
+            .cloned()
+            .flat_map(|wc| wc.expanded(program))
+            .collect()
+    }
+}
+
+trait WellFormed {
+    fn wf_clauses(&self, wf_predicate: ir::WellFormed, program: &ir::Program)
+        -> Vec<ir::ProgramClause>;
+}
+
+impl<T: ExpandWhereClauses> WellFormed for ir::Binders<T> {
+    fn wf_clauses(&self, wf_predicate: ir::WellFormed, program: &ir::Program)
+        -> Vec<ir::ProgramClause>
+    {
+        let where_clauses = self.value.expanded_where_clauses(program);
+
+        let wf = ir::ProgramClause {
+            implication: self.map_ref(|_| {
+                ir::ProgramClauseImplication {
+                    consequence: wf_predicate.clone().cast(),
+                    conditions: where_clauses.iter().cloned().casted().collect(),
+                }
+            }),
+            fallback_clause: false,
+        };
+
+        let mut clauses = vec![wf];
+        for cond in where_clauses {
+            clauses.push(ir::ProgramClause {
+                implication: self.map_ref(|_| {
+                    ir::ProgramClauseImplication {
+                        consequence: cond,
+                        conditions: vec![wf_predicate.clone().cast()]
+                    }
+                }),
+                fallback_clause: false,
+            });
+        }
+
+        clauses
+    }
+}
+
 impl ir::StructDatum {
     fn to_program_clauses(&self, program: &ir::Program) -> Vec<ir::ProgramClause> {
         // Given:
@@ -1027,34 +1089,13 @@ impl ir::StructDatum {
         // we generate the following clause:
         //
         //    for<?T> WF(Foo<?T>) :- WF(?T), (?T: Eq), WF(?T: Eq).
+        //    for<?T> (?T: Eq) :- WF(Foo<?T>).
+        //    for<?T> WF(?T: Eq) :- WF(Foo<?T>).
 
-        let wf = ir::ProgramClause {
-            implication: self.binders.map_ref(|bound_datum| {
-                ir::ProgramClauseImplication {
-                    consequence: ir::WellFormed::Ty(bound_datum.self_ty.clone().cast()).cast(),
-
-                    conditions: {
-                        let tys = bound_datum.self_ty
-                                             .parameters
-                                             .iter()
-                                             .filter_map(|pk| pk.as_ref().ty())
-                                             .cloned()
-                                             .map(|ty| ir::WellFormed::Ty(ty))
-                                             .casted();
-
-                        let where_clauses = bound_datum.where_clauses.iter()
-                                                       .cloned()
-                                                       .flat_map(|wc| wc.expanded(program))
-                                                       .casted();
-
-                        tys.chain(where_clauses).collect()
-                    }
-                }
-            }),
-            fallback_clause: false,
-        };
-
-        vec![wf]
+        self.binders.wf_clauses(
+            ir::WellFormed::Ty(self.binders.value.self_ty.clone().cast()),
+            program
+        )
     }
 }
 
@@ -1076,48 +1117,10 @@ impl ir::TraitDatum {
         //    for<?Self, ?T> (?Self: Eq<T>) :- WF(?Self: Ord<T>)
         //    for<?Self, ?T> WF(?Self: Ord<?T>) :- WF(?Self: Ord<T>)
 
-        let where_clauses = self.binders.value.where_clauses
-            .iter()
-            .cloned()
-            .flat_map(|wc| wc.expanded(program))
-            .collect::<Vec<_>>();
-        
-        let wf = ir::WellFormed::TraitRef(self.binders.value.trait_ref.clone());
-
-        let clauses = ir::ProgramClause {
-            implication: self.binders.map_ref(|bound| {
-                ir::ProgramClauseImplication {
-                    consequence: wf.clone().cast(),
-
-                    conditions: {
-                        let tys = bound.trait_ref.parameters
-                                                 .iter()
-                                                 .filter_map(|pk| pk.as_ref().ty())
-                                                 .cloned()
-                                                 .map(|ty| ir::WellFormed::Ty(ty))
-                                                 .casted();
-
-                        tys.chain(where_clauses.iter().cloned().casted()).collect()
-                    }
-                }
-            }),
-            fallback_clause: false,
-        };
-
-        let mut clauses = vec![clauses];
-        for wc in where_clauses {
-            clauses.push(ir::ProgramClause {
-                implication: self.binders.map_ref(|_| {
-                    ir::ProgramClauseImplication {
-                        consequence: wc,
-                        conditions: vec![wf.clone().cast()]
-                    }
-                }),
-                fallback_clause: false,
-            });
-        }
-
-        clauses
+        self.binders.wf_clauses(
+            ir::WellFormed::TraitRef(self.binders.value.trait_ref.clone().cast()),
+            program
+        )
     }
 }
 
diff --git a/src/solve/test.rs b/src/solve/test.rs
index 19132b001db..308e7fee429 100644
--- a/src/solve/test.rs
+++ b/src/solve/test.rs
@@ -131,10 +131,11 @@ fn prove_forall() {
             trait Marker { }
             impl<T> Marker for Vec<T> { }
 
-            trait Clone { }
-            impl Clone for Foo { }
+            trait Eq<T> { }
+            trait Ord<T> where Self: Eq<T> { }
 
-            impl<T> Clone for Vec<T> where T: Clone { }
+            impl<T> Eq<Vec<T>> for Vec<T> where T: Eq<T> { }
+            impl<T> Ord<Vec<T>> for Vec<T> where T: Ord<T> { }
         }
 
         goal {
@@ -164,19 +165,19 @@ fn prove_forall() {
             "Unique; substitution [], lifetime constraints []"
         }
 
-        // Here, we don't know that `T: Clone`, so we can't prove that
-        // `Vec<T>: Clone`.
+        // Here, we don't know that `T: Eq<T>`, so we can't prove that
+        // `Vec<T>: Eq<Vec<T>>`.
         goal {
-            forall<T> { Vec<T>: Clone }
+            forall<T> { Vec<T>: Eq<Vec<T>> }
         } yields {
-            "CannotProve"
+            "No possible solution"
         }
 
-        // Here, we do know that `T: Clone`, so we can.
+        // Here, we do know that `T: Eq`, so we can.
         goal {
             forall<T> {
-                if (T: Clone) {
-                    Vec<T>: Clone
+                if (T: Eq<T>) {
+                    Vec<T>: Eq<Vec<T>>
                 }
             }
         } yields {
@@ -184,16 +185,26 @@ fn prove_forall() {
         }
 
         // This fails because we used `if_raw`, and hence we do not
-        // know that `WF(T: Clone)` holds.
+        // know that `WF(T: Ord<T>)` hence `T: Eq<T>` holds.
         goal {
             forall<T> {
-                if_raw (T: Clone) {
-                    Vec<T>: Clone
+                if_raw (T: Ord<T>) {
+                    Vec<T>: Ord<Vec<T>>
                 }
             }
         } yields {
             "CannotProve"
         }
+
+        goal {
+            forall<T> {
+                if (T: Ord<T>) {
+                    Vec<T>: Ord<Vec<T>>
+                }
+            }
+        } yields {
+            "Unique"
+        }
     }
 }
 
@@ -1539,10 +1550,9 @@ fn coinductive_semantics() {
             "CannotProve"
         }
 
-        // `WellFormed(T)` because of the hand-written impl for `Ptr<T>`.
         goal {
             forall<T> {
-                if (WellFormed(T), T: Send) {
+                if (T: Send) {
                     List<T>: Send
                 }
             }
@@ -1596,3 +1606,66 @@ fn mixed_semantics() {
         }
     }
 }
+
+#[test]
+fn implied_bounds() {
+    test! {
+        program {
+            trait Hash { }
+            struct Set<K> where K: Hash { }
+
+            struct NotHash<T> { }
+
+            struct i32 { }
+            impl Hash for i32 { }
+
+            trait Eq<T> { }
+            trait Ord<T> where Self: Eq<T> { }
+
+            struct Ordered<U> where U: Ord<U> { }
+        }
+
+        // We know that `Set<K>` is well-formed so `K` must implement `Hash`.
+        goal {
+            forall<K> {
+                if (WellFormed(Set<K>)) {
+                    K: Hash
+                }
+            }
+        } yields {
+            "Unique"
+        }
+
+        // The following function:
+        // ```
+        // fn foo<T>(arg: Set<NotHash<T>>) {
+        //     /* assume that WellFormed(Set<NotHash<T>>) inside here */
+        // }
+        // ```
+        // cannot be called whatever the value of `T` is because
+        // there is no `Hash` impl for `NotHash<T>` hence `Set<NotHash<T>>`
+        // cannot be well-formed.
+        //
+        // Since `NotHash<T>` is a local type, a local negative
+        // reasoning is allowed and the following query fails. We can then issue
+        // a warning saying that the function cannot be called.
+        goal {
+            exists<T> {
+                WellFormed(Set<NotHash<T>>)
+            }
+        } yields {
+            "No possible solution"
+        }
+
+        // Transitive implied bounds
+        goal {
+            forall<U> {
+                if (WellFormed(Ordered<U>)) {
+                    U: Eq<U>
+                }
+            }
+        } yields {
+            "Unique"
+        }
+    }
+}