diff --git a/Lib/NETList.v b/Lib/NETList.v
index 7ed6072e..1af5d07a 100644
--- a/Lib/NETList.v
+++ b/Lib/NETList.v
@@ -19,7 +19,7 @@ Inductive netlist {A : Type} (B : A → A → Type) : A → A → Type :=
 Derive Signature NoConfusion NoConfusionHom Subterm for netlist.
 
 Arguments tfin {A B i j} x.
-Arguments tadd {A B i} j {k} x xs.
+Arguments tadd {A B i} j {k} _ _.
 
 Notation "x :::: xs" := (tadd _ x xs) (at level 60, right associativity).
 
diff --git a/Lib/TList.v b/Lib/TList.v
index dbaeb297..5511592e 100644
--- a/Lib/TList.v
+++ b/Lib/TList.v
@@ -35,7 +35,7 @@ Next Obligation.
 Defined.
 
 Arguments tnil {A B i}.
-Arguments tcons {A B i} j {k} x xs.
+Arguments tcons {A B i} j {k} _ _.
 
 Notation "x ::: xs" := (tcons _ x xs) (at level 60, right associativity).