From 8e143c5285cde1f31aa8322b9b0c7869567b06d8 Mon Sep 17 00:00:00 2001
From: Niels van der Weide <n.vanderweide@science.ru.nl>
Date: Tue, 19 Sep 2017 17:22:15 +0200
Subject: [PATCH] Cleaning in iso

---
 FiniteSets/list_representation/isomorphism.v | 18 +++++-------------
 FiniteSets/list_representation/properties.v  | 20 ++++++++++----------
 2 files changed, 15 insertions(+), 23 deletions(-)

diff --git a/FiniteSets/list_representation/isomorphism.v b/FiniteSets/list_representation/isomorphism.v
index 5a16b63..e835ef9 100644
--- a/FiniteSets/list_representation/isomorphism.v
+++ b/FiniteSets/list_representation/isomorphism.v
@@ -5,15 +5,7 @@ Require Import list_representation list_representation.operations
 Require Import kuratowski.kuratowski_sets.
 
 Section Iso.
-  Context {A : Type}.
-  Context `{Univalence}.
-
-  Definition dupl' (a : A) (X : FSet A) :
-    {|a|} ∪ {|a|} ∪ X = {|a|} ∪ X := assoc _ _ _ @ ap (∪ X) (idem _).
-  
-  Definition comm' (a b : A) (X : FSet A) :
-    {|a|} ∪ {|b|} ∪ X = {|b|} ∪ {|a|} ∪ X :=
-    assoc _ _ _ @ ap (∪ X) (comm _ _) @ (assoc _ _ _)^.
+  Context {A : Type} `{Univalence}.
 
   Definition FSetC_to_FSet: FSetC A -> FSet A.
   Proof.
@@ -21,10 +13,10 @@ Section Iso.
     - apply E.
     - intros a x.
       apply ({|a|} ∪ x).
-    - intros. cbn.
-      apply dupl'.
-    - intros. cbn.
-      apply comm'.
+    - intros a X.
+      apply (assoc _ _ _ @ ap (∪ X) (idem _)).
+    - intros a X Y.
+      apply (assoc _ _ _ @ ap (∪ Y) (comm _ _) @ (assoc _ _ _)^).
   Defined.
 
   Definition FSet_to_FSetC: FSet A -> FSetC A.
diff --git a/FiniteSets/list_representation/properties.v b/FiniteSets/list_representation/properties.v
index a09187f..ab654f4 100644
--- a/FiniteSets/list_representation/properties.v
+++ b/FiniteSets/list_representation/properties.v
@@ -5,8 +5,8 @@ Require Import list_representation list_representation.operations.
 Section properties.
   Context {A : Type}.
 
-  Definition append_nl : forall (x: FSetC A), ∅ ∪ x = x
-    := fun _ => idpath.
+  Definition append_nl (x: FSetC A) : ∅ ∪ x = x
+    := idpath.
 
   Lemma append_nr : forall (x: FSetC A), x ∪ ∅ = x.
   Proof.
@@ -15,16 +15,16 @@ Section properties.
     - intros. apply (ap (fun y => a;;y) X).
   Defined.
 
-  Lemma append_assoc {H: Funext}:
+  Lemma append_assoc :
     forall (x y z: FSetC A), x ∪ (y ∪ z) = (x ∪ y) ∪ z.
   Proof.
-    hinduction
-    ; try (intros ; apply path_forall ; intro
-           ; apply path_forall ; intro ;  apply set_path2).
-    - reflexivity.
-    - intros a x HR y z.
-      specialize (HR y z).
-      apply (ap (fun y => a;;y) HR).
+    intros x y z.
+    hinduction x ; try (intros ; apply path_ishprop).
+    - cbn.
+      reflexivity.
+    - intros.
+      cbn.
+      f_ap.
   Defined.
 
   Lemma append_singleton: forall (a: A) (x: FSetC A),