From 461c02d790dbf9ee39a21a7a86eda9d932167c01 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Feb 2015 15:45:31 -0800
Subject: [PATCH] fix(tests/lean/hott/433): remove bogus comment, and use
 rewrite tactic

Fix an issue raised by Floris.
See discussion at
https://github.com/leanprover/lean/issues/433
---
 tests/lean/hott/433.hlean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/lean/hott/433.hlean b/tests/lean/hott/433.hlean
index 78a3eaa55..6bd932434 100644
--- a/tests/lean/hott/433.hlean
+++ b/tests/lean/hott/433.hlean
@@ -94,6 +94,7 @@ namespace pi
   definition transport_V [reducible] (P : A → Type) {x y : A} (p : x = y) (u : P y) : P x :=
   p⁻¹ ▹ u
 
+  open function
   protected definition functor_pi : (Π(a:A), B a) → (Π(a':A'), B' a') := (λg a', f1 a' (g (f0 a')))
   /- Equivalences -/
   definition isequiv_functor_pi [instance] (f0 : A' → A) (f1 : Π(a':A'), B (f0 a') → B' a')
@@ -109,8 +110,7 @@ namespace pi
   rewrite adj,
   rewrite -transport_compose,
   rewrite {f1 a' _}(ap_transport _ f1 _),
-  apply (transport_V (λx, sect f0 a' ▹ x = h a') (retr (f1 _) _)),
-  -- retr cannot be used as rewrite rule, the resulting type is not an equality
+  rewrite (retr (f1 _) _),
   apply apD,
   intro h, beta,
   apply path_pi, intro a, esimp,