From 0310101dd5c05fe7bf622ebd059ab9f352499b27 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Sun, 13 Oct 2024 17:55:40 +0100
Subject: [PATCH] lost again

---
 SSA/Experimental/Bits/Fast/FIniteStateMachineClean.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/SSA/Experimental/Bits/Fast/FIniteStateMachineClean.lean b/SSA/Experimental/Bits/Fast/FIniteStateMachineClean.lean
index 848c26875..b0452332e 100644
--- a/SSA/Experimental/Bits/Fast/FIniteStateMachineClean.lean
+++ b/SSA/Experimental/Bits/Fast/FIniteStateMachineClean.lean
@@ -669,3 +669,6 @@ lemma eval_and (xs : BitStreamProd (Fin 2)) (i : Nat) : and'.eval xs = (xs 0) &&
   --   · simp [h]
   --     sorry
   --   · sorry
+  unfold eval; unfold and'; unfold mkBinaryPredicate
+  simp only [Fin.isValue, Width.n.mk_eq]
+  sorry