diff --git a/quotation/_CoqProject.in b/quotation/_CoqProject.in
index deabd85f1..831c4d369 100644
--- a/quotation/_CoqProject.in
+++ b/quotation/_CoqProject.in
@@ -88,6 +88,7 @@ theories/ToTemplate/Template/LiftSubst.v
 theories/ToTemplate/Template/ReflectAst.v
 theories/ToTemplate/Template/TermEquality.v
 theories/ToTemplate/Template/Typing.v
+theories/ToTemplate/Template/TypingWf.v
 theories/ToTemplate/Template/UnivSubst.v
 theories/ToTemplate/Template/WfAst.v
 theories/ToTemplate/Utils/All_Forall.v
diff --git a/quotation/theories/ToTemplate/All.v b/quotation/theories/ToTemplate/All.v
index 030b0bb17..9c19423c8 100644
--- a/quotation/theories/ToTemplate/All.v
+++ b/quotation/theories/ToTemplate/All.v
@@ -1,7 +1,7 @@
 From MetaCoq.Common Require Import config.
 From MetaCoq.Template Require Import Ast Typing.
-From MetaCoq.Template Require WfAst (*WfTyping*).
-From MetaCoq.Quotation.ToTemplate.Template Require Ast Typing WfAst (*WfTyping*).
+From MetaCoq.Template Require WfAst TypingWf.
+From MetaCoq.Quotation.ToTemplate.Template Require Ast Typing WfAst TypingWf.
 
 (* without typing derivations *)
 Module Raw.
@@ -14,7 +14,7 @@ Module Raw.
   Module WfAst.
     Definition quote_wf {Σ t} : @WfAst.wf Σ t -> Ast.term := WfAst.quote_wf.
   End WfAst.
-  (* TODO: do we want anything from WfTyping? Is there anything else missing here? *)
+  (* TODO: do we want anything from TypingWf? Is there anything else missing here? *)
 End Raw.
 
 (* eventually we'll have proofs that the above definitions are well-typed *)
diff --git a/quotation/theories/ToTemplate/Template/TypingWf.v b/quotation/theories/ToTemplate/Template/TypingWf.v
new file mode 100644
index 000000000..0ca45b7c4
--- /dev/null
+++ b/quotation/theories/ToTemplate/Template/TypingWf.v
@@ -0,0 +1,8 @@
+From MetaCoq.Template Require Import TypingWf.
+From MetaCoq.Quotation.ToTemplate Require Import Init.
+From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init.
+From MetaCoq.Quotation.ToTemplate.Utils Require Import (hints) All_Forall.
+From MetaCoq.Quotation.ToTemplate.Common Require Import (hints) BasicAst.
+From MetaCoq.Quotation.ToTemplate.Template Require Import (hints) Ast WfAst.
+
+#[export] Instance quote_wf_inductive_body {Σ idecl} : ground_quotable (@wf_inductive_body Σ idecl) := ltac:(destruct 1; exact _).