From 7f76d7e6482231f692c4f9f0e68262a493de1270 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 6 Aug 2015 23:50:57 +0200
Subject: [PATCH] fix(tests): update test

---
 tests/lean/hott/433.hlean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/hott/433.hlean b/tests/lean/hott/433.hlean
index eaa162e8a..5cfd8ece8 100644
--- a/tests/lean/hott/433.hlean
+++ b/tests/lean/hott/433.hlean
@@ -108,7 +108,7 @@ namespace pi
   --first subgoal
   intro a', esimp,
   rewrite adj,
-  rewrite -transport_compose,
+  rewrite -tr_compose,
   rewrite {f1 a' _}(fn_tr_eq_tr_fn _ f1 _),
   rewrite (right_inv (f1 _) _),
   apply apd,