Tactics looping on Isabelle2021

[jaycech3n]

Certain tactics loop on Isabelle2021-RC3. Needs further investigation.

[jaycech3n]

Looks like this comes from changes to the substitution tactics in Isabelle2021. See

• https://isabelle.in.tum.de/dist/Isabelle2021/doc/NEWS.html on "proof method subst", as well as
• $ISABELE_HOME/src/Tools/eqsubst.ML).

This results in altered computation behavior of the typechecker and simplification methods in I/HoTT. The proofs can be manually patched for now; really we'll want a rewrite of the simplification code at some point.