From c7fe8cd257d454e797f8476143e512654459b745 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 24 Feb 2013 14:00:09 +0100
Subject: [PATCH] Some cleanup.
---
theories/list.v | 10 +---------
1 file changed, 1 insertion(+), 9 deletions(-)
diff --git a/theories/list.v b/theories/list.v
index 5447d05c..f40467c0 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -581,15 +581,7 @@ Proof.
* rewrite NoDup_nil.
setoid_rewrite elem_of_nil. naive_solver.
* rewrite !NoDup_cons.
- setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app.
-split.
-destruct IHl.
-intros [??].
-split.
- naive_solver.
-
- naive_solver.
-naive_solver.
+ setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app. naive_solver.
Qed.
Global Instance NoDup_proper:
--
GitLab