From 245b58ac8b6dda26005ae998e5d2cf61a069711c Mon Sep 17 00:00:00 2001
From: Olivier Laurent
Date: Fri, 24 Apr 2020 17:07:09 +0200
Subject: Symmetry in conclusions of List.map_eq_*   allow simplified iterated
 applications

---
 theories/Sorting/CPermutation.v | 5 ++---
 theories/Sorting/Permutation.v  | 1 -
 2 files changed, 2 insertions(+), 4 deletions(-)

(limited to 'theories/Sorting')

diff --git a/theories/Sorting/CPermutation.v b/theories/Sorting/CPermutation.v
index fac9cd1d6d..ddc835891c 100644
--- a/theories/Sorting/CPermutation.v
+++ b/theories/Sorting/CPermutation.v
@@ -235,9 +235,8 @@ induction m as [| b m]; intros l HC.
   apply CPermutation_nil in HC; inversion HC.
 - symmetry in HC.
   destruct (CPermutation_vs_cons_inv HC) as [m1 [m2 [-> Heq]]].
-  apply map_eq_app in Heq as [l1 [l1' [-> [-> Heq]]]].
-  symmetry in Heq.
-  apply map_eq_cons in Heq as [a [l1'' [-> [-> ->]]]].
+  apply map_eq_app in Heq as [l1 [l1' [-> [<- Heq]]]].
+  apply map_eq_cons in Heq as [a [l1'' [-> [<- <-]]]].
   exists (a :: l1'' ++ l1); split.
   + now simpl; rewrite map_app.
   + now rewrite app_comm_cons.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index ffef8a216d..1dd9285412 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -552,7 +552,6 @@ Proof.
   - symmetry in HP.
     destruct (Permutation_vs_cons_inv HP) as [l3 [l4 Heq]].
     destruct (map_eq_app _ _ _ _ Heq) as [l1' [l2' [Heq1 [Heq2 Heq3]]]]; subst.
-    symmetry in Heq3.
     destruct (map_eq_cons _ _ Heq3) as [b [l1'' [Heq1' [Heq2' Heq3']]]]; subst.
     rewrite map_app in HP; simpl in HP.
     symmetry in HP.
-- 
cgit v1.2.3