diff --git a/crates/formality-prove/src/prove/prove_via.rs b/crates/formality-prove/src/prove/prove_via.rs
index c3c190a6..4ddbd463 100644
--- a/crates/formality-prove/src/prove/prove_via.rs
+++ b/crates/formality-prove/src/prove/prove_via.rs
@@ -7,6 +7,12 @@ use crate::{
 };
 
 judgment_fn! {
+    /// Check whether the where-clause `via` (which is one of the `assumptions` that are in in scope)
+    /// can be used to prove `goal` (the thing we are trying to prove).
+    ///
+    /// This is equivalent to the "elaboration" of the environment that takes place in rustc,
+    /// but done lazilly. For example, if you have `where T: Eq` then you can clearly prove `T: Eq`
+    /// but you can also prove `T: PartialEq` because `trait Eq: PartialEq`.
     pub fn prove_via(
         _decls: Decls,
         env: Env,
@@ -17,7 +23,9 @@ judgment_fn! {
         debug(goal, via, assumptions, env)
 
         (
+            // `c` = "clause", the name for something that we are assuming is true.
             (let (skel_c, parameters_c) = pred_1.debone())
+            // `g` = "goal, the name for something that we are trying to prove.
             (let (skel_g, parameters_g) = pred_2.debone())
             (if skel_c == skel_g)!
             (prove(decls, env, assumptions, Wcs::all_eq(parameters_c, parameters_g)) => c)
@@ -34,16 +42,21 @@ judgment_fn! {
             (prove_via(_decls, env, _assumptions, WcData::Relation(rel_1), WcData::Relation(rel_2)) => Constraints::none(env))
         )
 
+        // If you have `where for<'a> T: Trait<'a>` then you can prove `T: Trait<'b>` for any `'b`.
         (
             (let (env, subst) = env.existential_substitution(&binder))
             (let via1 = binder.instantiate_with(&subst).unwrap())
+            // Try to prove `T: Trait<?a> == goal`.
             (prove_via(decls, env, assumptions, via1, goal) => c)
             ----------------------------- ("forall")
             (prove_via(decls, env, assumptions, WcData::ForAll(binder), goal) => c.pop_subst(&subst))
         )
 
+        // If you have `where if (T: Debug) T: Foo` (not in Rust but it should be...)...
         (
+            // if the goal is `T: Foo`...
             (prove_via(&decls, env, &assumptions, wc_consequence, goal) => c)
+            // ...and we can prove `T: Debug`... then it holds.
             (prove_after(&decls, c, &assumptions, &wc_condition) => c)
             ----------------------------- ("implies")
             (prove_via(decls, env, assumptions, WcData::Implies(wc_condition, wc_consequence), goal) => c)
diff --git a/crates/formality-types/src/grammar/wc.rs b/crates/formality-types/src/grammar/wc.rs
index eae2a680..c85361ad 100644
--- a/crates/formality-types/src/grammar/wc.rs
+++ b/crates/formality-types/src/grammar/wc.rs
@@ -121,12 +121,16 @@ impl Wc {
 
 #[term]
 pub enum WcData {
+    /// Means the built-in relation holds.
     #[cast]
     Relation(Relation),
 
+    /// Means the predicate holds.
     #[cast]
     Predicate(Predicate),
 
+    // Equivalent to `for<'a>` except that it can also express `for<ty T>` and so forth:
+    // means `$v0` is true for any value of the bound variables (e.g., `'a` or `T`).
     #[grammar(for $v0)]
     ForAll(Binder<Wc>),