diff --git a/doc/invargent-manual.pdf b/doc/invargent-manual.pdf
index 40a2600..9cd91fb 100644
Binary files a/doc/invargent-manual.pdf and b/doc/invargent-manual.pdf differ
diff --git a/doc/invargent-manual.tm b/doc/invargent-manual.tm
index f730a1e..7161b59 100644
--- a/doc/invargent-manual.tm
+++ b/doc/invargent-manual.tm
@@ -1142,6 +1142,12 @@
   because InvarGenT, noticing the failure, generates an OCaml source with
   more type information, as if the <verbatim|-full_annot> option was used.
 
+  The example <verbatim|liquid_fft_simpler.gadt> contains assertions, but
+  despite them is nearly as hard as <verbatim|liquid_fft.gadt>. It needs the
+  option <verbatim|-same_with_assertions> to not switch to settings tuned for
+  cases where assertions capture the harder aspects of the invariants to
+  infer.
+
   Unfortunately, inference fails for some examples regardless of parameters
   setting. We discuss them in the next section.
 
@@ -1376,10 +1382,16 @@
   with the option <verbatim|-prefer_bound_to_local>. Additionally, we can
   relax the constraint on the processed portion of the matrix, coming from
   the restriction on the matrix size intended in the original source of the
-  <verbatim|liquid_gauss_harder.gadt> example. In
-  <verbatim|liquid_gauss.gadt>, the whole matrix is processed and the
-  inferred type is most general, under the default settings -- no need to
-  pass any options to InvarGenT.
+  FFT examples. In <verbatim|liquid_gauss.gadt>, the whole matrix is
+  processed and the inferred type is most general, under the default settings
+  -- no need to pass any options to InvarGenT. The reason
+  <verbatim|liquid_gauss_harder.gadt> is too difficult for InvarGenT is that
+  the nesting interferes with the propagation of use-site constraints to the
+  postcondition of the nested definition (the <verbatim|loop> inside
+  <verbatim|rowMax>). Inference works for
+  <verbatim|liquid_gauss_harder_asserted.gadt>, because the assertion
+  provides the required information to infer the <verbatim|rowMax> invariants
+  directly.
 </body>
 
 <\initial>
diff --git a/examples/liquid_gauss_harder.gadt b/examples/liquid_gauss_harder.gadt
index 906f269..03210ed 100644
--- a/examples/liquid_gauss_harder.gadt
+++ b/examples/liquid_gauss_harder.gadt
@@ -88,7 +88,7 @@ let rowElim r s n i =
 let gauss data =
   let n = matrix_dim1 data in
 
-  let rec rowMax i =
+  let rec rowMax = efunction i ->
     let x = fabs (matrix_get data i i) in
     let rec loop j x mx =
       eif j + 1 <= n then
diff --git a/examples/liquid_gauss_harder_asserted.gadt b/examples/liquid_gauss_harder_asserted.gadt
index d8ef87a..4d9ff98 100644
--- a/examples/liquid_gauss_harder_asserted.gadt
+++ b/examples/liquid_gauss_harder_asserted.gadt
@@ -87,12 +87,11 @@ let rowElim r s n i =
 
 let gauss data =
   let n = matrix_dim1 data in
-  assert num n + 1 <= matrix_dim2 data;
-  assert num matrix_dim2 data <= n + 1;
 
-  let rec rowMax i =
+  let rec rowMax = efunction i ->
     let x = fabs (matrix_get data i i) in
     let rec loop j x mx =
+      assert num mx + 1 <= n;
       eif j + 1 <= n then
         let y = fabs (matrix_get data j i) in
         eif (less x y) then loop (j+1) y j
diff --git a/examples/liquid_gauss_harder_asserted.gadti.target b/examples/liquid_gauss_harder_asserted.gadti.target
index caa45d5..2ece992 100644
--- a/examples/liquid_gauss_harder_asserted.gadti.target
+++ b/examples/liquid_gauss_harder_asserted.gadti.target
@@ -71,4 +71,4 @@ val rowElim :
    ∀i, j, k, n[0 ≤ n ∧ n + 1 ≤ i ∧ k ≤ i ∧ k ≤ j].
    Array (Float, j) → Array (Float, i) → Num k → Num n → ()
 
-val gauss : ∀n[1 ≤ n]. Matrix (n, n + 1) → ()
+val gauss : ∀k, n[1 ≤ n ∧ n + 1 ≤ k]. Matrix (n, k) → ()
diff --git a/src/InvarGenTTest.ml b/src/InvarGenTTest.ml
index 6b851ae..012312a 100644
--- a/src/InvarGenTTest.ml
+++ b/src/InvarGenTTest.ml
@@ -673,12 +673,11 @@ let tests = "InvarGenT" >::: [
            test_case "liquid_gauss_asserted" ());
       "liquid_gauss_harder_asserted" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_gauss_harder_asserted" ());
       "liquid_gauss_harder" >::
         (fun () ->
-           todo "FIXME";
+           todo "Too hard for current InvarGenT";
            skip_if !debug "debug";
            test_case "liquid_gauss_harder" ());
       "liquid_fft_ffor" >::