Lift blocks into defs

boogie-org · Dec 17, 2024 · 5d146d2 · 5d146d2
1 parent 9ac5e18
commit 5d146d2
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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