michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/data/finset/basic): cleanup proof

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-10 18:19:16 -07:00
parent 8aa634378e
commit 8fbe22f263
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/data/finset/basic.lean
View file

@ -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 assert P : to_nodup_list_of_nodup n = to_nodup_list l, from
begin begin
rewrite [↑to_nodup_list, ↑to_nodup_list_of_nodup], rewrite [↑to_nodup_list, ↑to_nodup_list_of_nodup],
generalize (@nodup_erase_dup A h l), congruence,
rewrite [erase_dup_eq_of_nodup n], intro x, apply congr_arg (subtype.tag l), rewrite [erase_dup_eq_of_nodup n]
apply proof_irrel
end, end,
quot.sound (eq.subst P !setoid.refl) quot.sound (eq.subst P !setoid.refl)