From 38a64bae76234256a2c9f2f57127c22213d698f3 Mon Sep 17 00:00:00 2001
From: Niels van der Weide <n.vanderweide@science.ru.nl>
Date: Thu, 28 Sep 2017 14:45:54 +0200
Subject: [PATCH] Simplification in proof of append_union

---
 FiniteSets/implementations/lists.v | 30 ++++++++++++++++++++++--------
 1 file changed, 22 insertions(+), 8 deletions(-)

diff --git a/FiniteSets/implementations/lists.v b/FiniteSets/implementations/lists.v
index f577a3a..2f86750 100644
--- a/FiniteSets/implementations/lists.v
+++ b/FiniteSets/implementations/lists.v
@@ -77,17 +77,31 @@ Section ListToSet.
     nr {|a|}.
 
   Lemma append_union (l1 l2 : list A) :
-    list_to_set A (union l1 l2) = (list_to_set A l1) ∪ (list_to_set A l2).
+    list_to_set A (list_union _ l1 l2) = (list_to_set A l1) ∪ (list_to_set A l2).
   Proof.
-    induction l1 ; induction l2 ; cbn.
+    induction l1 ; simpl.
     - apply (nl _)^.
-    - apply (nl _)^.
-    - rewrite IHl1.
-      apply assoc.
-    - rewrite IHl1.
-      cbn.
-      apply assoc.
+    - rewrite IHl1, assoc.
+      reflexivity.
   Defined.
+
+  Fixpoint reverse (l : list A) : list A :=
+    match l with
+    | nil => nil
+    | cons a l => list_union _ (reverse l) {|a|}
+    end.
+
+  Lemma reverse_set (l : list A) :
+    list_to_set A l = list_to_set A (reverse l).
+  Proof.
+    induction l ; simpl.
+    - reflexivity.
+    - rewrite append_union, ?IHl.
+      simpl.
+      rewrite nr.
+      apply comm.
+  Defined.
+    
 End ListToSet.
 
 Section lists_are_sets.