diff --git a/crates/formality-check/src/where_clauses.rs b/crates/formality-check/src/where_clauses.rs
index 77fc6af4..88b5cfe1 100644
--- a/crates/formality-check/src/where_clauses.rs
+++ b/crates/formality-check/src/where_clauses.rs
@@ -37,6 +37,10 @@ impl super::Check<'_> {
                     assumptions,
                     trait_id.with(self_ty, parameters),
                 ),
+            WhereClauseData::AliasEq(alias_ty, ty) => {
+                self.prove_parameter_well_formed(in_env, &assumptions, alias_ty)?;
+                self.prove_parameter_well_formed(in_env, &assumptions, ty)
+            }
             WhereClauseData::Outlives(a, b) => {
                 self.prove_parameter_well_formed(in_env, &assumptions, a)?;
                 self.prove_parameter_well_formed(in_env, assumptions, b)
diff --git a/crates/formality-prove/src/prove/constraints.rs b/crates/formality-prove/src/prove/constraints.rs
index ba85296c..ebfd9087 100644
--- a/crates/formality-prove/src/prove/constraints.rs
+++ b/crates/formality-prove/src/prove/constraints.rs
@@ -81,7 +81,8 @@ impl Constraints {
     ///
     /// * `self` -- the constraints from solving `A`
     /// * `c2` -- the constraints from solving `B` (after applying substitution from `self` to `B`)
-    pub fn seq(&self, c2: impl Upcast<Constraints>) -> Constraints {
+    pub fn seq(&self, c2: impl Upcast<Constraints> + std::fmt::Debug) -> Constraints {
+        dbg!(&self, &c2);
         let c2: Constraints = c2.upcast();
 
         self.assert_valid();
@@ -110,7 +111,7 @@ impl Constraints {
         Constraints {
             env: c2.env,
             known_true: self.known_true && c2.known_true,
-            substitution: c1_substitution.into_iter().chain(c2.substitution).collect(),
+            substitution: dbg!(c1_substitution.into_iter().chain(c2.substitution).collect()),
         }
     }
 
diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs
index 6e86521d..2197f4d5 100644
--- a/crates/formality-prove/src/prove/prove_wc.rs
+++ b/crates/formality-prove/src/prove/prove_wc.rs
@@ -58,7 +58,7 @@ judgment_fn! {
             (prove_after(&decls, c, co_assumptions, &i.where_clause) => c)
             (prove_after(&decls, c, &assumptions, &t.where_clause) => c)
             ----------------------------- ("positive impl")
-            (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
+            (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => dbg!(c).pop_subst(&subst))
         )
 
         (
@@ -78,6 +78,12 @@ judgment_fn! {
             (prove_wc(decls, env, assumptions, Predicate::NotImplemented(trait_ref)) => c.pop_subst(&subst))
         )
 
+        (
+            (prove_eq(decls, env, assumptions, alias_ty, ty) => c)
+            ----------------------------- ("alias eq")
+            (prove_wc(decls, env, assumptions, Predicate::AliasEq(alias_ty, ty)) => c)
+        )
+
         (
             (decls.trait_invariants() => ti)
             (let (env, subst) = env.existential_substitution(&ti.binder))
diff --git a/crates/formality-prove/src/prove/prove_wf.rs b/crates/formality-prove/src/prove/prove_wf.rs
index 0355e4f9..feadda7c 100644
--- a/crates/formality-prove/src/prove/prove_wf.rs
+++ b/crates/formality-prove/src/prove/prove_wf.rs
@@ -1,6 +1,6 @@
 use formality_types::{
-    grammar::{ConstData, Parameter, RigidName, RigidTy, UniversalVar, Wcs},
-    judgment_fn,
+    grammar::{ConstData, Parameter, RigidName, RigidTy, UniversalVar, Wcs, AliasTy, Parameters, AliasName},
+    judgment_fn, collections::Set,
 };
 
 use crate::{decls::Decls, prove::combinators::for_all};
@@ -39,10 +39,35 @@ judgment_fn! {
             (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::ScalarId(_), parameters }) => c)
         )
 
+        (
+            (for_all(&decls, &env, &assumptions, &parameters, &prove_wf) => c)
+            --- ("integers and booleans")
+            (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::AdtId(_), parameters }) => c)
+        )
+
         (
             (prove_wf(&decls, &env, &assumptions, ty) => c)
             --- ("rigid constants")
             (prove_wf(decls, env, assumptions, ConstData::Value(_, ty)) => c)
         )
+
+        (
+            (prove_alias_wf(&decls, &env, &assumptions, name, parameters) => c)
+            --- ("aliases")
+            (prove_wf(decls, env, assumptions, AliasTy { name, parameters }) => c)
+        )
     }
 }
+
+pub fn prove_alias_wf(
+    decls: &Decls,
+    env: &Env,
+    assumptions: &Wcs,
+    _name: AliasName,
+    parameters: Parameters,
+) -> Set<Constraints> {
+    tracing::debug!(?_name, ?parameters);
+
+    // FIXME: verify self type implements trait
+    for_all(decls, env, assumptions, &parameters, &prove_wf)
+}
diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs
index f9698bb0..33da1b4b 100644
--- a/crates/formality-rust/src/grammar.rs
+++ b/crates/formality-rust/src/grammar.rs
@@ -5,7 +5,7 @@ use formality_types::{
     cast::Upcast,
     grammar::{
         AdtId, AssociatedItemId, Binder, Const, CrateId, Fallible, FieldId, FnId, Lt, Parameter,
-        TraitId, TraitRef, Ty, Wc,
+        TraitId, TraitRef, Ty, Wc, AliasTy,
     },
     term::Term,
 };
@@ -325,6 +325,7 @@ impl WhereClause {
                     .not_implemented()
                     .upcast(),
             ),
+            WhereClauseData::AliasEq(_, _) => None,
             WhereClauseData::Outlives(_, _) => None,
             WhereClauseData::ForAll(binder) => {
                 let (vars, where_clause) = binder.open();
@@ -341,6 +342,9 @@ pub enum WhereClauseData {
     #[grammar($v0 : $v1 < $,v2 >)]
     IsImplemented(Ty, TraitId, Vec<Parameter>),
 
+    #[grammar($v0 => $v1)]
+    AliasEq(AliasTy, Ty),
+
     #[grammar($v0 : $v1)]
     Outlives(Parameter, Lt),
 
diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs
index 4325dd1d..04c271fb 100644
--- a/crates/formality-rust/src/prove.rs
+++ b/crates/formality-rust/src/prove.rs
@@ -377,6 +377,9 @@ impl ToWcs for WhereClause {
             WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => {
                 trait_id.with(self_ty, parameters).upcast()
             }
+            WhereClauseData::AliasEq(alias_ty, ty) => {
+                Predicate::AliasEq(alias_ty.clone(), ty.clone()).upcast()
+            }
             WhereClauseData::Outlives(a, b) => Relation::outlives(a, b).upcast(),
             WhereClauseData::ForAll(binder) => {
                 let (vars, wc) = binder.open();
diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs
index e5558fd1..220e2c0f 100644
--- a/crates/formality-types/src/grammar/formulas.rs
+++ b/crates/formality-types/src/grammar/formulas.rs
@@ -4,6 +4,8 @@ use crate::cast::To;
 use crate::cast::Upcast;
 use crate::cast_impl;
 
+use super::AliasName;
+use super::AliasTy;
 use super::Const;
 use super::Parameter;
 use super::Parameters;
@@ -23,6 +25,9 @@ pub enum Predicate {
     #[grammar(!$v0)]
     NotImplemented(TraitRef),
 
+    #[cast]
+    AliasEq(AliasTy, Ty),
+
     #[grammar(@WellFormedTraitRef($v0))]
     WellFormedTraitRef(TraitRef),
 
@@ -80,6 +85,7 @@ impl Parameter {
 pub enum Skeleton {
     IsImplemented(TraitId),
     NotImplemented(TraitId),
+    AliasEq(AliasName),
     WellFormed,
     WellFormedTraitRef(TraitId),
     IsLocal(TraitId),
@@ -110,6 +116,15 @@ impl Predicate {
                 Skeleton::NotImplemented(trait_id.clone()),
                 parameters.clone(),
             ),
+            Predicate::AliasEq(AliasTy { name, parameters }, ty) => {
+                let mut params = parameters.clone();
+                params.push(ty.clone().upcast());
+                (
+                    Skeleton::AliasEq(name.clone()),
+                    params,
+                )
+                
+            }
             Predicate::WellFormedTraitRef(TraitRef {
                 trait_id,
                 parameters,
diff --git a/fixme_tests/basic--where-clauses.rs b/fixme_tests/basic--where-clauses.rs
deleted file mode 100644
index 602eb153..00000000
--- a/fixme_tests/basic--where-clauses.rs
+++ /dev/null
@@ -1,51 +0,0 @@
-#![cfg(FIXME)]
-#![allow(non_snake_case)]
-
-#[test]
-#[ignore]
-fn test_universal() {
-    expect_test::expect![[r#"
-        Err(
-            Error {
-                context: "check_trait(WellFormed)",
-                source: Error {
-                    context: "prove_where_clause_well_formed([for_all(<ty> is_implemented(A((rigid (scalar u32)), ^ty0_0)))] => for_all(<ty> is_implemented(A((rigid (scalar u32)), ^ty0_0)))",
-                    source: Error {
-                        context: "prove_where_clause_well_formed([for_all(<ty> is_implemented(A((rigid (scalar u32)), ^ty0_0)))] => is_implemented(A((rigid (scalar u32)), !tyU(2)_0))",
-                        source: "could not prove `well_formed_trait_ref(A((rigid (scalar u32)), !tyU(2)_0))` given `[\n    for_all(<ty> is_implemented(A((rigid (scalar u32)), ^ty0_0))),\n]`",
-                    },
-                },
-            },
-        )
-    "#]]
-    .assert_debug_eq(&formality_rust::test_program_ok(
-        "[
-            crate core {
-                trait A<ty T> where [T: B<>] { }
-
-                trait B<> where [] { }
-
-                trait WellFormed<> where [for<ty T> u32: A<T>] { }
-            }
-        ]",
-    ));
-
-    expect_test::expect![[r#"
-        Ok(
-            (),
-        )
-    "#]]
-    .assert_debug_eq(&formality_rust::test_program_ok(
-        "[
-            crate core {
-                trait A<ty T> where [T: B<>] { }
-
-                trait B<> where [] { }
-
-                trait WellFormed<> where [for<ty T> u32: A<T>] { }
-
-                impl <ty T> B<> for T where [] {}
-            }
-        ]",
-    ));
-}
diff --git a/src/lib.rs b/src/lib.rs
index ccb9029a..82ee1e12 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -45,9 +45,11 @@ pub fn test_program_ok(input: &str) -> anyhow::Result<()> {
 }
 
 pub fn test_where_clause(program: &str, assertion: &str) -> anyhow::Result<Set<Constraints>> {
-    let program: Program = try_term(program)?;
-    check_all_crates(&program)?;
-    let assertion: Arc<TestAssertion> = try_term(assertion)?;
-    let decls = program.to_prove_decls();
-    Ok(formality_prove::test_util::test_prove(decls, assertion))
+    formality_core::with_tracing_logs(|| {
+        let program: Program = try_term(program)?;
+        check_all_crates(&program)?;
+        let assertion: Arc<TestAssertion> = try_term(assertion)?;
+        let decls = program.to_prove_decls();
+        Ok(formality_prove::test_util::test_prove(decls, assertion))
+    })
 }
diff --git a/tests/projection.rs b/tests/projection.rs
new file mode 100644
index 00000000..7010da35
--- /dev/null
+++ b/tests/projection.rs
@@ -0,0 +1,287 @@
+use formality::test_where_clause;
+
+const NORMALIZE_BASIC: &str = "[
+    crate test {
+        trait Iterator<> where [] {
+            type Item<> : [] where [];
+        }
+
+        struct Vec<ty T> where [] {}
+
+        struct Foo<> where [] {}
+
+        impl<ty T> Iterator<> for Vec<T> where [] {
+            type Item<> = T where [];
+        }
+    }
+]";
+
+#[test]
+fn normalize_basic() {
+    expect_test::expect![[r#"
+        Ok(
+            {
+                Constraints {
+                    env: Env {
+                        variables: [
+                            !ty_1,
+                            ?ty_2,
+                        ],
+                        coherence_mode: false,
+                    },
+                    known_true: true,
+                    substitution: {
+                        ?ty_2 => (alias (Iterator :: Item) (rigid (adt Vec) !ty_1)),
+                    },
+                },
+                Constraints {
+                    env: Env {
+                        variables: [
+                            !ty_1,
+                            ?ty_2,
+                        ],
+                        coherence_mode: false,
+                    },
+                    known_true: true,
+                    substitution: {
+                        ?ty_2 => !ty_1,
+                    },
+                },
+            },
+        )
+    "#]]
+    .assert_debug_eq(&test_where_clause(
+        NORMALIZE_BASIC,
+        "forall<ty T> exists<ty U> {} => { <Vec<T> as Iterator>::Item<> = U }",
+    ));
+
+    expect_test::expect![[r#"
+        Ok(
+            {
+                Constraints {
+                    env: Env {
+                        variables: [
+                            !ty_1,
+                        ],
+                        coherence_mode: false,
+                    },
+                    known_true: true,
+                    substitution: {},
+                },
+            },
+        )
+    "#]]
+    .assert_debug_eq(&test_where_clause(
+        NORMALIZE_BASIC,
+        "forall<ty T> {} => { Iterator(Vec<T>), <Vec<T> as Iterator<>>::Item<> = T }",
+    ));
+
+    expect_test::expect![[r#"
+        Ok(
+            {
+                Constraints {
+                    env: Env {
+                        variables: [
+                            !ty_1,
+                        ],
+                        coherence_mode: false,
+                    },
+                    known_true: true,
+                    substitution: {},
+                },
+            },
+        )
+    "#]]
+    .assert_debug_eq(&test_where_clause(
+        NORMALIZE_BASIC,
+        "forall<ty T> { Iterator(T), <T as Iterator<>>::Item<> = Foo } => { <T as Iterator<>>::Item<> = Foo }",
+    ));
+
+    expect_test::expect![[r#"
+        Ok(
+            {
+                Constraints {
+                    env: Env {
+                        variables: [
+                            !ty_1,
+                            ?ty_2,
+                        ],
+                        coherence_mode: false,
+                    },
+                    known_true: true,
+                    substitution: {
+                        ?ty_2 => (alias (Iterator :: Item) !ty_1),
+                    },
+                },
+            },
+        )
+    "#]]
+    .assert_debug_eq(&test_where_clause(
+        NORMALIZE_BASIC,
+        "forall<ty T> exists<ty U> { Iterator(T) } => { <T as Iterator<>>::Item<> = U }",
+    ));
+
+    expect_test::expect![[r#"
+        Ok(
+            {
+                Constraints {
+                    env: Env {
+                        variables: [
+                            !ty_1,
+                        ],
+                        coherence_mode: false,
+                    },
+                    known_true: true,
+                    substitution: {},
+                },
+            },
+        )
+    "#]]
+    .assert_debug_eq(&test_where_clause(
+        NORMALIZE_BASIC,
+        "forall<ty T> { Iterator(T) } => { <T as Iterator<>>::Item<> = <T as Iterator<>>::Item<> }",
+    ));
+
+    expect_test::expect![[r#"
+        Ok(
+            {
+                Constraints {
+                    env: Env {
+                        variables: [
+                            !ty_1,
+                            ?ty_2,
+                        ],
+                        coherence_mode: false,
+                    },
+                    known_true: true,
+                    substitution: {
+                        ?ty_2 => !ty_1,
+                    },
+                },
+                Constraints {
+                    env: Env {
+                        variables: [
+                            !ty_1,
+                            ?ty_3,
+                            ?ty_2,
+                        ],
+                        coherence_mode: false,
+                    },
+                    known_true: true,
+                    substitution: {
+                        ?ty_2 => (rigid (adt Vec) (alias (Iterator :: Item) !ty_1)),
+                        ?ty_3 => (alias (Iterator :: Item) !ty_1),
+                    },
+                },
+            },
+        )
+    "#]]
+    .assert_debug_eq(&test_where_clause(
+        NORMALIZE_BASIC,
+        "forall<ty T> exists<ty U> { Iterator(T) } => { <T as Iterator<>>::Item<> = <U as Iterator<>>::Item<> }",
+    ));
+}
+
+const NORMALIZE_INTO_ITERATOR: &str = "[
+    crate test {
+        trait IntoIterator<> where [] {
+            type Item<> : [] where [];
+        }
+
+        trait Iterator<> where [] {
+            type Item<> : [] where [];
+        }
+
+        struct Vec<ty T> where [] {}
+
+        struct Foo<> where [] {}
+
+        impl<ty T> IntoIterator<> for Vec<T> where [] {
+            type Item<> = T where [];
+        }
+
+        impl<ty T> IntoIterator<> for T where [ T: Iterator<> ] {
+            type Item<> = <T as Iterator>::Item<> where [];
+        }
+    }
+]";
+
+#[test]
+fn normalize_into_iterator() {
+    expect_test::expect![[r#"
+        Ok(
+            {
+                Constraints {
+                    env: Env {
+                        variables: [
+                            !ty_1,
+                            ?ty_2,
+                        ],
+                        coherence_mode: false,
+                    },
+                    known_true: true,
+                    substitution: {
+                        ?ty_2 => (alias (IntoIterator :: Item) (rigid (adt Vec) !ty_1)),
+                    },
+                },
+                Constraints {
+                    env: Env {
+                        variables: [
+                            !ty_1,
+                            ?ty_2,
+                        ],
+                        coherence_mode: false,
+                    },
+                    known_true: true,
+                    substitution: {
+                        ?ty_2 => !ty_1,
+                    },
+                },
+            },
+        )
+    "#]]
+    .assert_debug_eq(&test_where_clause(
+        NORMALIZE_INTO_ITERATOR,
+        "forall<ty T> exists<ty U> {} => { <Vec<T> as IntoIterator>::Item<> = U }",
+    ));
+}
+
+const PROJECTION_EQUALITY: &str = "[
+    crate test {
+        trait Trait1<> where [] {
+            type Type<> : [] where [];
+        }
+        trait Trait2<ty T> where [] {}
+        impl<ty T, ty U> Trait2<T> for U where [ U: Trait1<>, (alias (Trait1::Type) S) => T ] {}
+        struct S<> where [] {}
+        impl<> Trait1<> for S<> where [] {
+            type Type<> = u32 where [];
+        }
+    }
+]";
+
+
+#[test]
+fn projection_equality() {
+    expect_test::expect![[r#"
+        Ok(
+            {},
+        )
+    "#]]
+    .assert_debug_eq(&test_where_clause(
+        PROJECTION_EQUALITY,
+        "exists<ty U> {} => { S: Trait1<>, <S as Trait1<>>::Type<> = U }",
+    ));
+
+    /*
+    expect_test::expect![[r#"
+        Ok(
+            {},
+        )
+    "#]]
+    .assert_debug_eq(&test_where_clause(
+        PROJECTION_EQUALITY,
+        "exists<ty U> {} => { S: Trait2<U> }",
+    ));
+    */
+}
diff --git a/tests/ui/basic_where_clauses_fail.stderr b/tests/ui/basic_where_clauses_fail.stderr
new file mode 100644
index 00000000..2cd1a57f
--- /dev/null
+++ b/tests/ui/basic_where_clauses_fail.stderr
@@ -0,0 +1,6 @@
+Error: check_trait(WellFormed)
+
+Caused by:
+    0: prove_where_clause_well_formed(for <ty> (rigid (scalar u32)) : A < ^ty0_0 >)
+    1: prove_where_clause_well_formed((rigid (scalar u32)) : A < !ty_2 >)
+    2: failed to prove {@ WellFormedTraitRef(A((rigid (scalar u32)), !ty_2))} given {for <ty> A((rigid (scalar u32)), ^ty0_0)}, got {}
diff --git "a/tests/ui/basic_where_clauses_fail.\360\237\224\254" "b/tests/ui/basic_where_clauses_fail.\360\237\224\254"
new file mode 100644
index 00000000..57d080d6
--- /dev/null
+++ "b/tests/ui/basic_where_clauses_fail.\360\237\224\254"
@@ -0,0 +1,9 @@
+[
+    crate core {
+        trait A<ty T> where [T: B<>] { }
+
+        trait B<> where [] { }
+
+        trait WellFormed<> where [for<ty T> u32: A<T>] { }
+    }
+]
diff --git "a/tests/ui/basic_where_clauses_pass.\360\237\224\254" "b/tests/ui/basic_where_clauses_pass.\360\237\224\254"
new file mode 100644
index 00000000..cc9eb6f9
--- /dev/null
+++ "b/tests/ui/basic_where_clauses_pass.\360\237\224\254"
@@ -0,0 +1,12 @@
+//@check-pass
+[
+    crate core {
+        trait A<ty T> where [T: B<>] { }
+
+        trait B<> where [] { }
+
+        trait WellFormed<> where [for<ty T> u32: A<T>] { }
+
+        impl <ty T> B<> for T where [] {}
+    }
+]