From 9407e8cc665132f78342904c44a62ff9f1e0cd68 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 21 Jun 2019 13:07:33 +0200
Subject: [PATCH] Equalities for `list_merge` with `[]` arguments.

---
 theories/sorting.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/sorting.v b/theories/sorting.v
index f29e7b28..d1ff49a6 100644
--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -116,6 +116,10 @@ End sorted.
 Section merge_sort_correct.
   Context  {A} (R : relation A) `{∀ x y, Decision (R x y)}.
 
+  Lemma list_merge_nil_l l2 : list_merge R [] l2 = l2.
+  Proof. by destruct l2. Qed.
+  Lemma list_merge_nil_r l1 : list_merge R l1 [] = l1.
+  Proof. by destruct l1. Qed.
   Lemma list_merge_cons x1 x2 l1 l2 :
     list_merge R (x1 :: l1) (x2 :: l2) =
       if decide (R x1 x2) then x1 :: list_merge R l1 (x2 :: l2)
-- 
GitLab