diff --git a/.gitignore b/.gitignore
index 0240dcae454d0ebd6f911ff02f7be999e1b2110f..8c0aeb806b09cd18a1faa17752aef4261f947f0f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,6 +13,7 @@
 *.synctex.gz
 *.prv
 *.toc
+.lia.cache
 .#*
 auto
 *.fmt
diff --git a/coq/ra/adequacy.v b/coq/ra/adequacy.v
index c4891e4662f9a557b056bba70502732d580eb621..4f642801fbd66685d0a77684902c3814233d617d 100644
--- a/coq/ra/adequacy.v
+++ b/coq/ra/adequacy.v
@@ -13,14 +13,12 @@ Class basePreG Σ := BasePreG {
   base_preG_info :> inG Σ (authR Infos);
 }.
 
-Definition baseΣ : gFunctors := #[ownPΣ (language.state ra_lang); foundationΣ].
+Definition baseΣ : gFunctors := #[ownPΣ (language.state ra_lang);
+      GFunctor (authR Views);
+      GFunctor (authR Hists);
+      GFunctor (authR Infos)].
 Instance subG_basePreG {Σ} : subG baseΣ Σ → basePreG Σ.
-Proof.
-  intros [? [[? [? ?]%subG_inv]%subG_inv _]%subG_inv]%subG_inv. split; try apply _.
-  - apply (subG_inG _ _ s0).
-  - apply (subG_inG _ _ s1).
-  - apply (subG_inG _ _ s2).
-Qed.
+Proof. solve_inG. Qed.
 
 Definition to_view (σ : language.state ra_lang) : Views := (Excl <$> threads σ).
 Definition loc_sets (σ : language.state ra_lang) : gmap loc (gset message) :=
diff --git a/coq/ra/base/ghosts.v b/coq/ra/base/ghosts.v
index d4954460bdf9351ce7a40b6fecd8d8e99e563440..9e5e805e6a443cc49dbe41e9ced696e5b4ea2d87 100644
--- a/coq/ra/base/ghosts.v
+++ b/coq/ra/base/ghosts.v
@@ -32,16 +32,6 @@ Class foundationG Σ :=
 
 Definition AuthType {Σ} {T} (X : inG Σ (authR T)) := T.
 
-Definition foundationΣ : gFunctors :=
-  #[
-    GFunctor (constRF (authR Views));
-      GFunctor (constRF (authR Hists));
-      GFunctor (constRF (authR Infos))
-  ].
-(* Instance inGF_foundationG {Σ} : subG foundationΣ Σ → foundationG Σ. *)
-(* Proof. *)
-(* Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed. *)
-
 (* Todo: figure out why this is needed and get rid of it *)
 Global Instance foundationG_hist_insert `{foundationG Σ} : Insert loc (excl (gset (Val * View))) (AuthType foundationG_hist) := _.
 Global Instance foundationG_hist_singleton `{foundationG Σ} : SingletonM loc (excl (gset (Val * View))) (AuthType foundationG_hist) := _.
diff --git a/coq/ra/escrows.v b/coq/ra/escrows.v
index 74a982a3e21cceb9ee184f14158baefca6441340..b6f0377406fdb5bf1d4171aa598ba542d902072f 100644
--- a/coq/ra/escrows.v
+++ b/coq/ra/escrows.v
@@ -16,7 +16,7 @@ Definition absViewΣ : gFunctors :=
   #[ GFunctor (agreeRF ViewR) ].
 
 Instance subG_absViewΣ {Σ} : subG absViewΣ Σ → absViewG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Section AbstractView.
 
diff --git a/coq/ra/examples/circ_buffer.v b/coq/ra/examples/circ_buffer.v
index 13c88c9d81b3fbc106c46c8c1ed82fffc8aa0d35..de7dd5c067a7fb5130ae03cf0f7befb36d1d6e2c 100644
--- a/coq/ra/examples/circ_buffer.v
+++ b/coq/ra/examples/circ_buffer.v
@@ -53,7 +53,7 @@ Section CircBuffer.
   Definition cbΣ : gFunctors := #[GFunctor (constRF circBufR)].
 
   Instance subG_cbΣ {Σ} : subG cbΣ Σ → cbG Σ.
-  Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+  Proof. solve_inG. Qed.
 
   Section Interpretation.
     Context `{fG: !foundationG Σ, aG: !absViewG Σ, cirbG: !cbG Σ}.
diff --git a/coq/ra/examples/message_passing.v b/coq/ra/examples/message_passing.v
index 962254024c0180cd27eea734650ed76a4126826d..78b51bf3350bba11b269a89e93dd69f8ffb08f41 100644
--- a/coq/ra/examples/message_passing.v
+++ b/coq/ra/examples/message_passing.v
@@ -22,7 +22,7 @@ Class mpG Σ := MpG { mp_tokG :> inG Σ (exclR unitC) }.
 Definition mpΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
 
 Instance subG_mpΣ {Σ} : subG mpΣ Σ → mpG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Section Interpretation.
   Context `{foundationG Σ} `{!absViewG Σ} `{mespG : !mpG Σ}.
diff --git a/coq/ra/examples/ticket_lock.v b/coq/ra/examples/ticket_lock.v
index 0c834fb4c6617c759c15893fd759947b59357297..440b6beb5014c817697e7c6bea61e197cbed7fbe 100644
--- a/coq/ra/examples/ticket_lock.v
+++ b/coq/ra/examples/ticket_lock.v
@@ -15,7 +15,7 @@ Class tklG Σ := TklG { tkl_tokG :> inG Σ ticketLockR }.
 Definition tklΣ : gFunctors := #[GFunctor (constRF ticketLockR)].
 
 Instance subG_tklΣ {Σ} : subG tklΣ Σ → tklG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Section TicketLock.
 
diff --git a/coq/ra/gps/inst_shared.v b/coq/ra/gps/inst_shared.v
index 9cd14bb3441ba3de9ca36c0e7ecb257576677e2a..56d4ba1cb5edbe784ee2d0b8a6592c5c378e4e36 100644
--- a/coq/ra/gps/inst_shared.v
+++ b/coq/ra/gps/inst_shared.v
@@ -12,4 +12,4 @@ Notation gps_agreeG Σ Prtcl := (inG Σ (dec_agreeR (EqDecision0 := state_sort_e
 Definition gps_agreeΣ Prtcl (PF : protocol_facts Prtcl) : gFunctors := #[ GFunctor (constRF ((dec_agreeR (EqDecision0 := state_sort_eqdec Prtcl%type) (state_sort Prtcl)))) ].
 
 Instance subG_gps_agreeΣ Σ Prtcl PF : subG (gps_agreeΣ Prtcl PF) Σ → gps_agreeG Σ Prtcl.
-Proof. intros [? ?]%subG_inv. apply (subG_inG _ _ s). Qed.
\ No newline at end of file
+Proof. solve_inG. Qed.
diff --git a/coq/ra/gps/shared.v b/coq/ra/gps/shared.v
index 6c5494e1e1ea19206ef8f8edc7e29e4c016a4173..f72dec20940e05d06e0cb7faca5f843e27117033 100644
--- a/coq/ra/gps/shared.v
+++ b/coq/ra/gps/shared.v
@@ -81,12 +81,9 @@ Class gpsG Σ Prtcl (PF : protocol_facts Prtcl) :=
   }.
 Definition gpsΣ Prtcl (PF : protocol_facts Prtcl) : gFunctors :=
   #[ GFunctor (constRF stateR); GFunctor (constRF (authR (optionUR (prodR fracR (dec_agreeR (state_sort Prtcl)))))) ].
+
 Instance subG_gpsG {Σ} Prtcl PF : subG (gpsΣ Prtcl PF) Σ → gpsG Σ Prtcl PF.
-Proof.
-  intros [? [? ?]%subG_inv]%subG_inv. split; try apply _.
-  - apply (subG_inG _ _ s).
-  - apply (subG_inG _ _ s0).
-Qed.
+Proof. solve_inG. Qed.
 
 Arguments st_prst [_] _ /.
 Arguments st_val [_] _ /.
diff --git a/coq/ra/persistor.v b/coq/ra/persistor.v
index 72e16cf5065ea4edcebb4f7bae88e97ffeeffff9..c99e62afef091be66e4b52fa7f2f1a9248256240 100644
--- a/coq/ra/persistor.v
+++ b/coq/ra/persistor.v
@@ -27,7 +27,7 @@ Class persistorPreG Σ :=
     persistorPreG_perinfo :> inG Σ (authR PerInfos)
   }.
 Instance subG_persistorPreG {Σ} : subG persistorΣ Σ → persistorPreG Σ.
-Proof. intros [? ?]%subG_inv; constructor. apply (subG_inG _ _ s). Qed.
+Proof. solve_inG. Qed.
 
 Section Persistor.
   Context `{!foundationG Σ, !persistorG Σ}.
diff --git a/coq/ra/rsl.v b/coq/ra/rsl.v
index c33237a4d6483ee8848340498dccd807f611956f..76b77d52ddd97da10ac652299768a5be0ad2c60e 100644
--- a/coq/ra/rsl.v
+++ b/coq/ra/rsl.v
@@ -25,7 +25,7 @@ Definition rslΣ : gFunctors
  := #[stsΣ rsl_sts; savedPropΣ (ofe_funCF Z (ofe_funCF View idCF))].
 
 Instance subG_rslΣ {Σ} : subG rslΣ Σ → rslG Σ.
-Proof. intros [? [? _]%subG_inv]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Section proof.