Replace term reducibility in the logical relation by the diagonal of reducible term conversion

[kyoDralliam]

This PR removes the term reducibility predicate [ Γ ||- t : A | RA ] and replaces it with reflexive instance of the reducible term conversion [ Γ ||- t ≅ t : A | RA ]. Since we can show quite early on that the latter relation is a PER, witnesses of [ Γ ||- t ≅ u : A | RA ] imply both [ Γ ||- t ≅ t : A | RA ] and [ Γ ||- u ≅ u : A | RA ]. Overall, removing this component does remove a lot of redundancies present in the proofs.

[MevenBertrand]

Is this ready for merging? Should I try to rebase my refactoring branch on top of this one first, just to check I can survive it? (It should be fine since I almost don't touch the logical relation, but…)

[MevenBertrand]

Also, have thought about/tried removing reducibility of types? A priori, you could say that a pair of terms are reducibly convertible wrt. a proof that two types are reducibly convertible, rather than a proof that a given type is reducible?

[kyoDralliam]

Is this ready for merging? Should I try to rebase my refactoring branch on top of this one first, just to check I can survive it? (It should be fine since I almost don't touch the logical relation, but…)

I could do more cleanups, but unless anyone disagree with the changes in this PR, I think it can be merged.

[kyoDralliam]

Also, have thought about/tried removing reducibility of types? A priori, you could say that a pair of terms are reducibly convertible wrt. a proof that two types are reducibly convertible, rather than a proof that a given type is reducible?

I tried, and got stuck because the definition of reducibility and reducible conversion on terms employed reducible conversion of types in a way that wouldn't be strictly positive if I were to just replace reducibility of types by reducible conversion of the diagonal.

However, I have now a branch that does remove these depencies at the price of weakening slightly the logical relation (and it does not impact the end theorems), so I'll try again to remove the reducibility of types next.

[MevenBertrand]

I haven't looked at the proofs in details, but

• I'm sympathetic with the high-level goal
• a -2kLoC change seems like a good sign
• you're the expert in the logical relation anyway
  If there are clean-ups needed we can defer that later, I'd rather avoid bitrot.