Antal Spector-Zabusky

Oh, I see – regardless of whether `Mod.Tree` was an inductive type or a definition? Seems reasonable!

OK, e9c47a7 adds support for `redefine Axiom`, since I wanted that for `TrieMap` :-)

@sweirich Right now, we do that when we can. The issue here is that the two function take *different* implicit arguments (`{a}` vs. `{b}`), so we can't common them up....

This is very neat! After a quick look, it seems like the biggest issue with this would be introducing the proof obligation in the translation step, rather than the verification...

Sounds like a good plan. I'd recommend `polymorphic Mod.val` and either `cumulative Mod.val` or `polymorphic cumulative Mod.val` to be consistent with the current set of edits. We'll probably need to...

Actually, another thought: should we always enable universe polymorphism and/or cumulativity? What would be the ramifications of that? (With `Universe Polymorphism.` and/or `Set Polymorphic Inductive Cumulativity.`)

Ah, good point about the preamble. We could also switch to default polymorphic/edits for monomorphism, but it seems like there's no reason to do that – polymorphism seems to be...

How easy is this to work around?

@sweirich done, although I haven't looked into the details closely

Damn, that's true >_