diff --git a/Examples/Ffs.lean b/Examples/Ffs.lean
index de1c256..47efbb7 100644
--- a/Examples/Ffs.lean
+++ b/Examples/Ffs.lean
@@ -192,7 +192,9 @@ example : ffs_imp (i0, ()) = ffs_ref (i0, ()) := by
   unfold ffs_imp
   simp
   rw [runProc, runRes]
+  congr 1
 
   -- rw [ffs_imp]
 
   sorry
+  done