From d4dcb60b6f34aa94c48a25012ed2eff91baa41fb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 1 Jun 2021 16:52:12 +0200
Subject: [PATCH] Explicitly spell out lemma statement of some `Permutation`
 lemmas that we borrow from stdlib.

---
 theories/list.v | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index 426a5ce6..f2d9a5d0 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1697,9 +1697,13 @@ Lemma Permutation_nil l : l ≡ₚ [] ↔ l = [].
 Proof. split; [by intro; apply Permutation_nil | by intros ->]. Qed.
 Lemma Permutation_singleton l x : l ≡ₚ [x] ↔ l = [x].
 Proof. split; [by intro; apply Permutation_length_1_inv | by intros ->]. Qed.
-Definition Permutation_skip := @perm_skip A.
-Definition Permutation_swap := @perm_swap A.
-Definition Permutation_singleton_inj := @Permutation_length_1 A.
+
+Lemma Permutation_skip x l l' : l ≡ₚ l' → x :: l ≡ₚ x :: l'.
+Proof. apply perm_skip. Qed.
+Lemma Permutation_swap x y l : y :: x :: l ≡ₚ x :: y :: l.
+Proof. apply perm_swap. Qed.
+Lemma Permutation_singleton_inj x y : [x] ≡ₚ [y] → x = y.
+Proof. apply Permutation_length_1. Qed.
 
 Global Instance Permutation_cons x : Proper ((≡ₚ) ==> (≡ₚ)) (@cons A x).
 Proof. by constructor. Qed.
-- 
GitLab