From 2dc188a78b71739105ac799dffdfdb79647f6403 Mon Sep 17 00:00:00 2001
From: Stephanie Weirich <sweirich@cis.upenn.edu>
Date: Sat, 23 Apr 2016 14:06:06 -0400
Subject: [PATCH] restored usage of uniqness tactic

---
 CoqListFacts.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/CoqListFacts.v b/CoqListFacts.v
index 5ccd93b..06e2be9 100644
--- a/CoqListFacts.v
+++ b/CoqListFacts.v
@@ -230,14 +230,14 @@ Section Uniqueness_Of_SetoidList_Proofs.
 
   Theorem lelistA_unique :
     forall (x : A) (xs : list A) (p q : lelistA R x xs), p = q.
-  Proof. induction p using lelistA_ind'. Admitted.   (* was uniqueness 1 *)
+  Proof. induction p using lelistA_ind'; uniqueness 1. Qed. 
 
   Theorem sort_unique :
     forall (xs : list A) (p q : sort R xs), p = q.
-  Proof. induction p using sort_ind'. Admitted. (* uniqueness 1. apply lelistA_unique. Qed. *)
+  Proof. induction p using sort_ind'; uniqueness 1. apply lelistA_unique. Qed.
 
   Theorem eqlistA_unique :
     forall (xs ys : list A) (p q : eqlistA R xs ys), p = q.
-  Proof. induction p using eqlistA_ind'. Admitted. (* uniqueness 2. Qed. *)
+  Proof. induction p using eqlistA_ind'; uniqueness 2. Qed. 
 
 End Uniqueness_Of_SetoidList_Proofs.