From aace5c37cd60deaa05fd799fcfe9573b9ca24f83 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 1 Sep 2014 19:04:15 -0700 Subject: [PATCH] refactor(library/data/subtype): elaborator does not need help anymore (i.e., 'show'-expression) for this file Signed-off-by: Leonardo de Moura --- library/data/subtype.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/library/data/subtype.lean b/library/data/subtype.lean index ffd7103e0a..2a204b8782 100644 --- a/library/data/subtype.lean +++ b/library/data/subtype.lean @@ -27,13 +27,14 @@ section (H : ∀(x : A) (H1 : P x), Q (tag x H1)) : Q a := subtype_rec H a - theorem tag_irrelevant {a : A} (H1 H2 : P a) : tag a H1 = tag a H2 := refl (tag a H1) + theorem tag_irrelevant {a : A} (H1 H2 : P a) : tag a H1 = tag a H2 := + rfl - theorem tag_elt_of (a : subtype P) : Π(H : P (elt_of a)), tag (elt_of a) H = a := - subtype_destruct a (take (x : A) (H1 : P x) (H2 : P x), refl _) + theorem tag_elt_of (a : subtype P) : ∀(H : P (elt_of a)), tag (elt_of a) H = a := + subtype_destruct a (take (x : A) (H1 : P x) (H2 : P x), rfl) theorem tag_eq {a1 a2 : A} {H1 : P a1} {H2 : P a2} (H3 : a1 = a2) : tag a1 H1 = tag a2 H2 := - (show ∀(H2 : P a2), tag a1 H1 = tag a2 H2, from subst H3 (take H2, tag_irrelevant H1 H2)) H2 + subst H3 (take H2, tag_irrelevant H1 H2) H2 theorem subtype_eq {a1 a2 : {x, P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 := subtype_destruct a1 (take x1 H1, subtype_destruct a2 (take x2 H2 H, tag_eq H))