diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 58e72cf04b57985773be26fa1f63d74df063dad9..e402dc73b900954a424559ec860b0ee55769d80f 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -2,6 +2,7 @@ From iris.program_logic Require Export hoare adequacy.
 From iris.algebra Require Import auth.
 From lrust.lang Require Export heap.
 From lrust.lang Require Import proofmode notation.
+Set Default Proof Using "Type".
 
 Class heapPreG Σ := HeapPreG {
   heap_preG_ownP :> ownPPreG lrust_lang Σ;
diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index 00d92652c508146332b832ea9a0e30a97ff035fd..a649ab181f49f124497c91ab00b2110513796fcd 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -1,6 +1,7 @@
 From lrust.lang Require Export lifting.
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
+Set Default Proof Using "Type".
 Import uPred.
 
 (** Define some derived forms, and derived lemmas about them. *)
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 679e3a9bdf438deacae375cc11a6dbb42c8eeb3b..a976118ab31bdad03cfe3f7206d9f50d6fa6c572 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -4,6 +4,7 @@ From iris.algebra Require Import csum excl auth.
 From iris.base_logic Require Import big_op lib.invariants lib.fractional.
 From iris.proofmode Require Export tactics.
 From lrust.lang Require Export lifting.
+Set Default Proof Using "Type".
 Import uPred.
 
 Definition heapN : namespace := nroot .@ "heap".
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index af91c92d719df2a6606c66a7cd9b2fcdba464c61..e770632fbf7d41725a99a49e31628cf26450cfb4 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -1,6 +1,7 @@
 From iris.program_logic Require Export language ectx_language ectxi_language.
 From iris.prelude Require Export strings.
 From iris.prelude Require Import gmap.
+Set Default Proof Using "Type".
 
 Open Scope Z_scope.
 
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index cfd392c0dd3578783a1f185236bdbaecbc0cd047..ede4cd0ff028549c572ffbdda03459cdf979eccd 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -3,6 +3,7 @@ From iris.program_logic Require Import ectx_lifting.
 From lrust.lang Require Export lang.
 From lrust.lang Require Import tactics.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 Import uPred.
 Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2.
 
diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index e65919f1c88aa0815726d06d95d72d67bdf6164a..f11083b0aa8fbbe8a96ef8d9dbdd6ecfc6dbb530 100644
--- a/theories/lang/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -1,6 +1,7 @@
 From iris.base_logic.lib Require Import namespaces.
 From lrust.lang Require Export notation.
 From lrust.lang Require Import heap proofmode.
+Set Default Proof Using "Type".
 
 Definition memcpy : val :=
   rec: "memcpy" ["dst";"len";"src"] :=
diff --git a/theories/lang/new_delete.v b/theories/lang/new_delete.v
index fa541f0f4eccd22afc97e422103213641772a8ee..5b5be8279fabfc7e849d40a5ba712e1df3cb5c90 100644
--- a/theories/lang/new_delete.v
+++ b/theories/lang/new_delete.v
@@ -1,6 +1,7 @@
 From iris.base_logic.lib Require Import namespaces.
 From lrust.lang Require Export notation.
 From lrust.lang Require Import heap proofmode memcpy.
+Set Default Proof Using "Type".
 
 Definition new : val :=
   λ: ["n"],
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index a47399b5d145fdac854bdb8e18f08680fc8f8c12..1caf26f4563ce4fdbd5295e008f31b95488aa489 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -1,4 +1,5 @@
 From lrust.lang Require Export derived.
+Set Default Proof Using "Type".
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitLoc : loc >-> base_lit.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index fb4d20e89692e4758c5581b997e1d180e304ea3e..44a89ce868a5cfebb040fa5062edd31f52b02c2c 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -2,6 +2,7 @@ From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
 From iris.base_logic Require Import namespaces.
 From lrust.lang Require Export wp_tactics heap.
+Set Default Proof Using "Type".
 Import uPred.
 
 Ltac wp_strip_later ::= iNext.
diff --git a/theories/lang/races.v b/theories/lang/races.v
index dc94392dab068d3bf2d6ee1b193b7322389e2576..c0b8b497e4f64f994cd87c900b3449372c2ee546 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -2,6 +2,7 @@ From iris.prelude Require Import gmap.
 From iris.program_logic Require Export hoare.
 From iris.program_logic Require Import adequacy.
 From lrust.lang Require Import tactics.
+Set Default Proof Using "Type".
 
 Inductive access_kind : Type := ReadAcc | WriteAcc | FreeAcc.
 
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index a622fddae6bdc74629e053f6937d395f8e138820..5767645f97ef27cebbde9e9758b5cd3f58d2cddf 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -1,5 +1,6 @@
 From iris.prelude Require Import fin_maps.
 From lrust.lang Require Export lang.
+Set Default Proof Using "Type".
 
 (** We define an alternative representation of expressions in which the
 embedding of values and closed expressions is explicit. By reification of
diff --git a/theories/lang/wp_tactics.v b/theories/lang/wp_tactics.v
index 12d8f8ca3265b674682c4a0340c1f59d27583d73..f4d6c053e41faa1a9a6143dccf5b077be750ee11 100644
--- a/theories/lang/wp_tactics.v
+++ b/theories/lang/wp_tactics.v
@@ -1,4 +1,5 @@
 From lrust.lang Require Export tactics derived.
+Set Default Proof Using "Type".
 Import uPred.
 
 (** wp-specific helper tactics *)
diff --git a/theories/lifetime/accessors.v b/theories/lifetime/accessors.v
index 14210f73bc4106af113f0cdeb202146fc30440aa..2f3b4b0381da371ff6ab9123ee76e34f6ee4d979 100644
--- a/theories/lifetime/accessors.v
+++ b/theories/lifetime/accessors.v
@@ -3,6 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
+Set Default Proof Using "Type".
 
 Section accessors.
 Context `{invG Σ, lftG Σ}.
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index b2bf7ce811f697d4038fc602338087cb393b3dcd..7ce44adae63e23c76305d04745456b27ef0f931e 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -4,6 +4,7 @@ From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Section borrow.
 Context `{invG Σ, lftG Σ}.
diff --git a/theories/lifetime/creation.v b/theories/lifetime/creation.v
index 5c4cb539aaddee477216f21653a3b4ec9af09581..e731f97ab0cbfbc106d5c67f765bd5a958e7265c 100644
--- a/theories/lifetime/creation.v
+++ b/theories/lifetime/creation.v
@@ -4,6 +4,7 @@ From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Section creation.
 Context `{invG Σ, lftG Σ}.
diff --git a/theories/lifetime/definitions.v b/theories/lifetime/definitions.v
index d98f4dd120fc4f9cfb45fc821bd135a61df8047a..ce443fd3d3d9cafee71d341be36168e73fc3b969 100644
--- a/theories/lifetime/definitions.v
+++ b/theories/lifetime/definitions.v
@@ -3,6 +3,7 @@ From iris.prelude Require Export gmultiset strings.
 From iris.base_logic.lib Require Export invariants.
 From iris.base_logic.lib Require Import boxes.
 From iris.base_logic Require Import big_op.
+Set Default Proof Using "Type".
 Import uPred.
 
 Definition lftN : namespace := nroot .@ "lft".
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index 73b28d1018be895950c35c637f3180878493133d..ecf3524f857dde16b22020a7daa9aa45160f9a74 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -1,6 +1,7 @@
 From lrust.lifetime Require Export primitive accessors faking.
 From lrust.lifetime Require Export raw_reborrow.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 (* TODO: the name derived makes no sense: reborrow/bor_unnest, which is proven
 in the model, depends on this file. *)
 
diff --git a/theories/lifetime/faking.v b/theories/lifetime/faking.v
index 7ee7bd10c7a57a2da837c76b5b28dbb6f0db8d0e..1def1f51ec0e86b8774c3613d5437f0700d47c11 100644
--- a/theories/lifetime/faking.v
+++ b/theories/lifetime/faking.v
@@ -3,6 +3,7 @@ From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Section faking.
 Context `{invG Σ, lftG Σ}.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 841ac12e746b6eecef9842d0130dc6821f4b715a..77084d69e77214874822756a6f371205600521cb 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -3,6 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import lib.fractional.
 From iris.algebra Require Import frac.
 From lrust.lifetime Require Export shr_borrow .
+Set Default Proof Using "Type".
 
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 16ae3d6943febf8c86dd2cd9592ff1553a70b74b..41a69f9e11845696b3a59b32397df9a86ef0b838 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -1,6 +1,7 @@
 From lrust.lifetime Require Export derived.
 From iris.base_logic.lib Require Export na_invariants.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Definition na_bor `{invG Σ, lftG Σ, na_invG Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index 235510a1decffa187497b69c678922a794ac62c8..7ed8780ac6c7e700fa276a22abff64e1fa2547b4 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/primitive.v
@@ -3,6 +3,7 @@ From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes fractional.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 Import uPred.
 
 Section primitive.
diff --git a/theories/lifetime/raw_reborrow.v b/theories/lifetime/raw_reborrow.v
index cde623f055df681dbd7a3117a9df0a4d5690b74e..7dbf4a55822586db929a57ced82becf433526a59 100644
--- a/theories/lifetime/raw_reborrow.v
+++ b/theories/lifetime/raw_reborrow.v
@@ -4,6 +4,7 @@ From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Section rebor.
 Context `{invG Σ, lftG Σ}.
diff --git a/theories/lifetime/reborrow.v b/theories/lifetime/reborrow.v
index b899064431bdbd8ea3ebe8967bf0020b8a9537e8..567d6b42ce593246b5f0d4e8c61a1c6c23245c83 100644
--- a/theories/lifetime/reborrow.v
+++ b/theories/lifetime/reborrow.v
@@ -4,6 +4,7 @@ From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Section reborrow.
 Context `{invG Σ, lftG Σ}.
diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
index 0df3676db4532358eb5731f343c4bb8ccddc9732..10a1473121b6cefac1c855f5d4b0160c1d9d2cb9 100644
--- a/theories/lifetime/shr_borrow.v
+++ b/theories/lifetime/shr_borrow.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Import gmap auth frac.
 From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Export derived.
+Set Default Proof Using "Type".
 
 (** Shared bors  *)
 Definition shr_bor `{invG Σ, lftG Σ} κ (P : iProp Σ) :=
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 9f8287886c684a5c1b2b5d17bb6d8725e5961cb9..60330dce46b38b9c91e798ee737689e0ddeda2bb 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -2,6 +2,7 @@ From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
+Set Default Proof Using "Type".
 
 Section bool.
   Context `{typeG Σ}.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 13baa93ed15529a043fba24ad74af5cfd99bf174..e105e2cdf43c26f9076dd432451a953a50d48040 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -4,6 +4,7 @@ From lrust.lifetime Require Import reborrow frac_borrow.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export uniq_bor shr_bor own.
 From lrust.typing Require Import lft_contexts type_context programs.
+Set Default Proof Using "Type".
 
 (** The rules for borrowing and derferencing borrowed non-Copy pointers are in
   a separate file so make sure that own.v and uniq_bor.v can be compiled
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 10926c2f8485acd1a98c234859c513949c9498af..853194869fe7717165c38e0eab5fe20a54e40d0d 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -3,6 +3,7 @@ From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
+Set Default Proof Using "Type".
 
 Section typing.
   Context `{typeG Σ}.
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index b3fb8b9529f1a1fc19fb3c130ace79a65cf45899..e239890bec89a9ee6fe241b53b3d8bd9019bd4f2 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -3,6 +3,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lang Require Import notation.
 From lrust.lifetime Require Import definitions.
 From lrust.typing Require Import type lft_contexts type_context.
+Set Default Proof Using "Type".
 
 Section cont_context_def.
   Context `{typeG Σ}.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 2cb0e1b48fb56843a3b439f99e5f5c899a1dd1e5..c8ca59f84fedddedd5efcb55c7add62bde7eb86a 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -1,5 +1,6 @@
 From lrust.lifetime Require Import definitions.
 From lrust.typing Require Export lft_contexts type bool.
+Set Default Proof Using "Type".
 
 Section fixpoint.
   Context `{typeG Σ}.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 95981845d64b986ec68d9833d2ad51b71ca35a46..709fe8b854ef0ad2aad7118e677ce7a1cab3629f 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -4,6 +4,7 @@ From iris.algebra Require Import vector.
 From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs cont.
+Set Default Proof Using "Type".
 
 Section fn.
   Context `{typeG Σ} {A : Type} {n : nat}.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 5b4cc7e398f50ead1853c3f83f69cfba14db0607..27d58cf40a12e26c9bf488b03a94918f76538f35 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -1,6 +1,7 @@
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import bool programs.
+Set Default Proof Using "Type".
 
 Section int.
   Context `{typeG Σ}.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 76e72e949161892315d50aa793dab0b5fb7c3e42..1fa4444ea08554e2900355c3c41da5fb44dbb67e 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -2,6 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import fractional.
 From lrust.lifetime Require Import derived borrow frac_borrow.
+Set Default Proof Using "Type".
 
 Inductive elctx_elt : Type :=
 | ELCtx_Alive (κ : lft)
diff --git a/theories/typing/own.v b/theories/typing/own.v
index a2a94267c8d71ae72a816c93ec8291576fe995a3..c095a2a744bbb9c975d011760e83795b8213fdb3 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -6,6 +6,7 @@ From lrust.lang Require Export new_delete.
 From lrust.lang Require Import memcpy.
 From lrust.typing Require Export type.
 From lrust.typing Require Import uninit type_context programs.
+Set Default Proof Using "Type".
 
 Section own.
   Context `{typeG Σ}.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 705ae108604ad8cec277027f098453c0701480e0..bed771821285edbe01b9f095f8eefdcc0e8422d6 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -2,6 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import list.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
+Set Default Proof Using "Type".
 
 Section product.
   Context `{typeG Σ}.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 261a2d369a0303213a973268657cdf7ad9696db1..b02d8d1d01747b079250786b47b4db983107303f 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -4,6 +4,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import type_context lft_contexts product own uniq_bor shr_bor.
+Set Default Proof Using "Type".
 
 Section product_split.
   Context `{typeG Σ}.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index e5ae5ee4f6f953afbcb58cf870b44fdff360f5f2..4ff553ea16b297b1309506047d6864d68d4661f8 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -3,6 +3,7 @@ From lrust.lang Require Export notation.
 From lrust.lang Require Import proofmode memcpy.
 From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
 From lrust.typing Require Export type lft_contexts type_context cont_context.
+Set Default Proof Using "Type".
 
 Section typing.
   Context `{typeG Σ}.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 789aaa3ee4fee0ddd5124afee2746c195d113625..23350e748c6ece89fb43c1bc7da2800f8d63ace0 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -3,6 +3,7 @@ From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Import frac_borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import lft_contexts type_context programs.
+Set Default Proof Using "Type".
 
 Section shr_bor.
   Context `{typeG Σ}.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 6cb8c72a6ea9dfa3ccd4b8c0b1ca5a05e40d2de8..330da63da8a2e96d3fe4f59fcfc16e3c2d79b9d6 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -3,6 +3,7 @@ From iris.algebra Require Import list.
 From iris.base_logic Require Import fractional.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
+Set Default Proof Using "Type".
 
 Section sum.
   Context `{typeG Σ}.
diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v
index b7e263d2614b440b95f8fe782a403c98cb376086..d770fb2a7fa3cada4b3ff1ad947b2669d2a5f679 100644
--- a/theories/typing/tests/get_x.v
+++ b/theories/typing/tests/get_x.v
@@ -2,6 +2,7 @@ From lrust.lifetime Require Import definitions.
 From lrust.lang Require Import new_delete.
 From lrust.typing Require Import programs product product_split own uniq_bor
                     shr_bor int function lft_contexts uninit cont.
+Set Default Proof Using "Type".
 
 Section get_x.
   Context `{typeG Σ}.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 88bb1ddd020c894e1be2c2b4072670a71e2ae203..8585d23063dbb300f9fabd75ff29490829fa9e61 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -3,6 +3,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lang Require Export proofmode notation.
 From lrust.lifetime Require Import borrow frac_borrow reborrow.
 From lrust.typing Require Import lft_contexts.
+Set Default Proof Using "Type".
 
 Class typeG Σ := TypeG {
   type_heapG :> heapG Σ;
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 9344e92e463c3102dd5f3feb4807269f7d8fefbb..741e0558253374799e280d8525c4d125f1aa6cc9 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -3,6 +3,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lang Require Import notation.
 From lrust.lifetime Require Import definitions.
 From lrust.typing Require Import type lft_contexts.
+Set Default Proof Using "Type".
 
 Definition path := expr.
 Bind Scope expr_scope with path.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index e523544d6f9da6c439304d3a7074da52e44e2485..eece54ef7b85f885d1f285bfc810caae8e1015e0 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -3,6 +3,7 @@ From lrust.lang Require Import heap memcpy.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export uninit uniq_bor shr_bor own sum.
 From lrust.typing Require Import lft_contexts type_context programs product.
+Set Default Proof Using "Type".
 
 Section case.
   Context `{typeG Σ}.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 6c25430d0fe34861655ee5d894d794874b2f5746..0dbfa1ea03788039d6adc479d934d5938ab8a817 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -1,6 +1,7 @@
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import product.
+Set Default Proof Using "Type".
 
 Section uninit.
   Context `{typeG Σ}.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 5920a3c2367eea80e508406be9d501bc66cf2eeb..8c776efa2fcffc5bb6abe2b9234bf067bc66508d 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -4,6 +4,7 @@ From lrust.lifetime Require Import borrow frac_borrow reborrow.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export type.
 From lrust.typing Require Import lft_contexts type_context shr_bor programs.
+Set Default Proof Using "Type".
 
 Section uniq_bor.
   Context `{typeG Σ}.