diff --git a/theories/typing/automation/solvers.v b/theories/typing/automation/solvers.v
index e4b5d7d6520adba33c80b110d4d68fadaa4e9a61..477582cda483b786bc69b3139ac5d47a4bb3b1f6 100644
--- a/theories/typing/automation/solvers.v
+++ b/theories/typing/automation/solvers.v
@@ -181,6 +181,7 @@ Ltac solve_rmovable :=
 Ltac solve_ty_layout_eq :=
   simpl;
   repeat lazymatch goal with
+    | |- ∀ _ : (), _ => case
     | |- ∀ _ : (_ * _), _ => case
     | |- ∀ _ : _, _ => move => ?
     end;