Added reverse permutation

Author: guilhermehas

CHANGELOG.md

@@ -3037,3 +3037,8 @@ This is a full list of proofs that have changed form to use irrelevant instance
   ```agda
   <-weakInduction-startingFrom : P i →  (∀ j → P (inject₁ j) → P (suc j)) → ∀ {j} → j ≥ i → P j
   ```
+
+* Added new function to `Data.List.Relation.Binary.Permutation.Propositional.Properties`
+  ```agda
+  ↭-reverse : (xs : List A) → reverse xs ↭ xs
+  ```

src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda

@@ -324,6 +324,18 @@ drop-∷ = drop-mid [] []
 ++↭ʳ++ []       ys = ↭-refl
 ++↭ʳ++ (x ∷ xs) ys = ↭-trans (↭-sym (shift x xs ys)) (++↭ʳ++ xs (x ∷ ys))
 
+------------------------------------------------------------------------
+-- reverse
+
+↭-reverse : (xs : List A) → reverse xs ↭ xs
+↭-reverse [] = ↭-refl
+↭-reverse (x ∷ xs) = begin
+  reverse (x ∷ xs) ≡⟨ Lₚ.unfold-reverse x xs ⟩
+  reverse xs ∷ʳ x ↭˘⟨ ∷↭∷ʳ x (reverse xs) ⟩
+  x ∷ reverse xs   ↭⟨ prep x (↭-reverse xs) ⟩
+  x ∷ xs ∎
+  where open PermutationReasoning
+
 ------------------------------------------------------------------------
 -- merge