From 8fbe22f2637f5614ff1592e688e9456a8cc80e78 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 10 Jun 2015 18:19:16 -0700 Subject: [PATCH] refactor(library/data/finset/basic): cleanup proof --- library/data/finset/basic.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean index 7a0c4c6c2..3045c593a 100644 --- a/library/data/finset/basic.lean +++ b/library/data/finset/basic.lean @@ -52,9 +52,8 @@ lemma to_finset_eq_of_nodup [h : decidable_eq A] {l : list A} (n : nodup l) : assert P : to_nodup_list_of_nodup n = to_nodup_list l, from begin rewrite [↑to_nodup_list, ↑to_nodup_list_of_nodup], - generalize (@nodup_erase_dup A h l), - rewrite [erase_dup_eq_of_nodup n], intro x, apply congr_arg (subtype.tag l), - apply proof_irrel + congruence, + rewrite [erase_dup_eq_of_nodup n] end, quot.sound (eq.subst P !setoid.refl)