`rec` based compilation in the equation compiler

[leodemoura]

The equation compiler currently supports the following compilation strategies

• brec_on (aka course of values recursion)
• well_founded recursion
• unbounded recursion for meta definitions
• Non recursive

However, none of the compilation approaches can be used when proving lemmas for inductive predicates. We cannot use brec_on because, in general, we cannot define the auxiliary type below for an inductive predicate. The issue is that most inductive predicates can only eliminate into Prop. So, we need another compilation strategy which uses the rec recursor instead of the more general brec_on.

Until this feature is implemented, users must use tactics to prove lemmas about inductive predicates.

[leodemoura]

The compilation strategy based on the primitive recursor rec is also useful when handling reflexive types. See #1620