Fix termination and performance issues with DecEq

[ana-pantilie]

Needs #7832

Termination fix

Removes the need for the TERMINATING pragma in the decEq definitions, Agda can now prove that they terminate.

Performance fix

The matching on refl inside decEq triggered normalization of terms when typechecking, which affected performance significantly, to the point of using more than 128GB of memory for the example @basetunnel and I worked on.

The example is an equality proof of the first AST to itself, from agda-certificates/cardano_constitution_Cardano_Constitution_Validator_Data_Sorted-b48sy0.agda-cert. This was the certificate produced for defaultConstitutionCode from cardano-constitution/src/Cardano/Constitution/Validator/Data/Sorted.hs.

For this particular example comparing cons was the most expensive, so avoiding matching on refl in the recursive call to decEq-⟦ t ⟧tag x x₁ inside decEq-TmCon did the trick.