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

fix(tests): update test

Browse source
This commit is contained in:
Floris van Doorn 2015-08-06 23:50:57 +02:00 committed by Leonardo de Moura
parent ad5cda48a8
commit 7f76d7e648
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/hott/433.hlean
View file

@ -108,7 +108,7 @@ namespace pi
--first subgoal --first subgoal
intro a', esimp, intro a', esimp,
rewrite adj, rewrite adj,
rewrite -transport_compose, rewrite -tr_compose,
rewrite {f1 a' _}(fn_tr_eq_tr_fn _ f1 _), rewrite {f1 a' _}(fn_tr_eq_tr_fn _ f1 _),
rewrite (right_inv (f1 _) _), rewrite (right_inv (f1 _) _),
apply apd, apply apd,