Here's some Ltac magic, as requested in https://github.com/HoTT/HoTT/pull/893. I think the comment on one_line_proof is now outdated; I'll leave it to you to clean that up. Let me know if anything here doesn't make sense.
Perhaps @mattam82 can explain why Unset Keyed Unification makes rewrite fail more quickly here, and if there's any way to fix that.
spitters
commented
6 years ago
Here's some Ltac magic, as requested in https://github.com/HoTT/HoTT/pull/893. I think the comment on
one_line_proofis now outdated; I'll leave it to you to clean that up. Let me know if anything here doesn't make sense.Perhaps @mattam82 can explain why
Unset Keyed Unificationmakesrewritefail more quickly here, and if there's any way to fix that.