1 files changed, 5 insertions, 6 deletions
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.
+  induction bs using map_ind; [done|].
-  - done.
+  unfold nonrecs.
-  - unfold nonrecs.
+  rewrite fmap_insert.
-    rewrite fmap_insert.
+  rewrite omap_insert_Some with (y := x); try done.
-    rewrite omap_insert_Some with (y := x); try done.
+  by f_equal.
-    by f_equal.
 Qed.
 Lemma rec_subst_nonrec_fmap bs : rec_subst (B_Nonrec <$> bs) = bs.

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 :=
14		14
15	Lemma nonrecs_nonrec_fmap bs : nonrecs (B_Nonrec <$> bs) = bs.	15	Lemma nonrecs_nonrec_fmap bs : nonrecs (B_Nonrec <$> bs) = bs.
16	Proof.	16	Proof.
17	induction bs using map_ind.	17	induction bs using map_ind; [done\|].
18	- done.	18	unfold nonrecs.
19	- unfold nonrecs.	19	rewrite fmap_insert.
20	rewrite fmap_insert.	20	rewrite omap_insert_Some with (y := x); try done.
21	rewrite omap_insert_Some with (y := x); try done.	21	by f_equal.
22	by f_equal.
23	Qed.	22	Qed.
24		23
25	Lemma rec_subst_nonrec_fmap bs : rec_subst (B_Nonrec <$> bs) = bs.	24	Lemma rec_subst_nonrec_fmap bs : rec_subst (B_Nonrec <$> bs) = bs.