From 4598e77a9406d8040357c943a05dd1ab939932db Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Thu, 27 Jun 2024 01:56:05 +0200
Subject: Tidy up project

* Write README.md
* Add LICENSE
* Clean up some theorems and proofs
---
 shared.v | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'shared.v')

diff --git a/shared.v b/shared.v
index 8e9484f..2365c9d 100644
--- a/shared.v
+++ b/shared.v
@@ -14,12 +14,11 @@ Definition nonrecs : gmap string b_rhs → gmap string expr :=
 
 Lemma nonrecs_nonrec_fmap bs : nonrecs (B_Nonrec <$> bs) = bs.
 Proof.
-  induction bs using map_ind.
-  - done.
-  - unfold nonrecs.
-    rewrite fmap_insert.
-    rewrite omap_insert_Some with (y := x); try done.
-    by f_equal.
+  induction bs using map_ind; [done|].
+  unfold nonrecs.
+  rewrite fmap_insert.
+  rewrite omap_insert_Some with (y := x); try done.
+  by f_equal.
 Qed.
 
 Lemma rec_subst_nonrec_fmap bs : rec_subst (B_Nonrec <$> bs) = bs.
-- 
cgit v1.2.3