chore: unfold to fix proof

opencompl · May 22, 2024 · b5f5a6e · b5f5a6e
1 parent 8651154
commit b5f5a6e
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/SSA/Projects/DCE/DCE.lean b/SSA/Projects/DCE/DCE.lean
@@ -278,7 +278,10 @@ def Com.deleteVar? (DEL : Deleted Γ delv Γ') (com : Com d Γ .pure t) :
     match Var.tryDelete? DEL v with
     | .none => .none
     | .some ⟨v, hv⟩ =>
-      .some ⟨.ret v, hv⟩
+      .some ⟨.ret v, by
+        unfold Ctxt.Valuation.eval at hv
+        simp [hv]
+      ⟩
   | .lete (α := ω) e body =>
     match Com.deleteVar? (Deleted.snoc DEL) body with
     | .none => .none