list.v.diff

diff --git a/theories/list.v b/theories/list.v
index 2f1db8e..a200405 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2988,6 +2988,11 @@ Section setoid.
   Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
   Global Instance list_lookup_proper i : Proper ((≡@{list A}) ==> (≡)) (lookup i).
   Proof. induction i; destruct 1; simpl; try constructor; auto. Qed.
+  Global Instance list_lookup_total_proper `{!Inhabited A} i :
+    Proper ((≡@{list A}) ==> (≡)) (lookup_total i).
+  Proof.
+    induction i; destruct 1; simpl; try auto. Abort.
+    
   Global Instance list_alter_proper f i :
     Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡@{list A})) (alter f i).
   Proof. intros. induction i; destruct 1; constructor; eauto. Qed.