Commit 2020-08-15 07:22 c1a5283b

refactor(data/list/tfae): tfae.out (#3774) This version of tfae.out has slightly better automatic reduction behavior: if h : [a, b, c].tfae then the original of h.out 1 2 proves [a, b, c].nth_le 1 _ <-> [a, b, c].nth_le 2 _ while the new version of h.out 1 2 proves b <-> c. These are the same, of course, and you can mostly use them interchangeably, but the second one is a bit nicer to look at (and possibly works better with e.g. subsequent rewrites).