diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index ccd63aa523d59c4a0ca73ef82f6944a726d52ae9..3dc30ee425c11f16f50a83022cd33caa6d2820bb 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -28,9 +28,8 @@ Module invG.
     disabled_inPreG :> inG Σ (gset_disjR positive);
   }.
 
-Instance subG_invΣ {Σ} : subG invΣ Σ → invPreG Σ.
-Proof. solve_inG. Qed.
-
+  Instance subG_invΣ {Σ} : subG invΣ Σ → invPreG Σ.
+  Proof. solve_inG. Qed.
 End invG.
 Import invG.