From bd82f5e81c17ccafe233bbc64c8888620dd7e795 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 12 Jul 2014 19:08:53 +0100
Subject: [PATCH] chore(library/standard/piext): cleanup hcongr proof

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 library/standard/piext.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/library/standard/piext.lean b/library/standard/piext.lean
index 3ad193725..611e4b78c 100644
--- a/library/standard/piext.lean
+++ b/library/standard/piext.lean
@@ -27,8 +27,8 @@ theorem hcongr1 {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x}
 
 theorem hcongr {A A' : Type} {B : A → Type} {B' : A' → Type} {f : Π x, B x} {f' : Π x, B' x} {a : A} {a' : A'}
                (Hff' : f == f') (Haa' : a == a') : f a == f' a'
-:= have H : ∀ (B B' : A → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a, from
+:= have H1 : ∀ (B B' : A → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a, from
      take B B' f f' e, hcongr1 a e,
-   @hsubst _ _ _ _ (fun (X : Type) (x : X),
-       ∀ (B : A → Type) (B' : X → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' x)
-       Haa' H B B' f f' Hff'
+   have H2 : ∀ (B : A → Type) (B' : A' → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a', from
+     hsubst Haa' H1,
+   H2 B B' f f' Hff'