Record inheritance about aya-dev HOT 6 OPEN

We need to implement aya-prover/aya-prover-proto#150 (which, I guess, is related to aya-prover/aya-prover-proto#128) first

from aya-dev.

So we should implement in this order:

• typeclass w/o inheritance
• coercion as typeclass
• record inheritance through coercion
• typeclass inheritance through record inheritance

from aya-dev.

... and built-in definitions.

from aya-dev.

I mean pragmas that make definitions interact with built-in features

from aya-dev.

So we should implement in this order:

• typeclass w/o inheritance
• coercion as typeclass
• record inheritance through coercion
• typeclass inheritance through record inheritance

No, in this order:

• aya-prover/aya-prover-proto#503
• as listed above

from aya-dev.

In Arend, they have this:

class Functor F
 | bleh

class Monad F extends Functor
 | blah

instance ok : Functor Bla
 | bleh

instance ko : Monad Bla
 | Functor => ok
 | bleh => *&^%$#$%^&

from aya-dev.