Tesla Zhang‮

We should do index erasure in an IR and run the shape matcher again. `Vec` will be matched with `List` and `Fin`/`∈` will be matched with `Nat`.

> `A` should be only compiled once by the way Yes, we do have that now.

> > We should compute SCC of dependencies before compiling the library. > > The libraries won't depend on each other Are you sure? What if they declare so?

Looks like it's closed by #978

FYI https://github.com/github/linguist/pull/4777/

No longer exist in the new version

Deprecated due to the redesign of `coe`

Ref: https://github.com/aya-prover/aya-dev/issues/449

We temporarily give up `Prop` due to its complication

https://github.com/JetBrains/arend-lib/commit/8f7339486a8d0d3cb8b2d76da6edf38f86e535ac