diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index f0a672be02f9df230cad0d2ee1846cc46127d4b2..70130e8260ea2f7ecaebad4ceb0be5054bbfee12 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -21,8 +21,11 @@ Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
 Ltac solve_inG :=
   (* Get all assumptions *)
   intros;
-  (* Unfold the top-level xΣ *)
+  (* Unfold the top-level xΣ. We need to support this to be a function. *)
   lazymatch goal with
+  | H : subG (?xΣ _ _ _ _) _ |- _ => try unfold xΣ in H
+  | H : subG (?xΣ _ _ _) _ |- _ => try unfold xΣ in H
+  | H : subG (?xΣ _ _) _ |- _ => try unfold xΣ in H
   | H : subG (?xΣ _) _ |- _ => try unfold xΣ in H
   | H : subG ?xΣ _ |- _ => try unfold xΣ in H
   end;