Fix issue #6930: Allow recursion on proofs again

[andreasabel]

• Fix Termination checking with --prop: change in 2.6.4 compared with 2.6.3 #6930: Revert "Respect DontCare in termination checker (Respect DontCare in termination checker #6639)"
• Test cases for Respect DontCare in termination checker #6639 (impredicative prop) and Termination checking with --prop: change in 2.6.4 compared with 2.6.3 #6930 (inductive prop)

TODO:

• CHANGELOG entry

[jespercockx]

I don't mind reverting the change, but people using --prop should be aware that this implies an additional principle which is incompatible with impredicative Prop. Perhaps you could add the comment from the test case to the user manual for Prop too?

[plt-amy]

Please see my objection here. I'm uneasy about allowing what is the termination "using the wrong formula to get the right answer" as default behaviour, though I would be fine with having the old behaviour under a flag for compatibility.

[plt-amy]

After discussion in today's meeting we agreed that it's not worth including the fix for Prop since

• The underlying issue in the termination checker would also affect impredicative Set, which is also consistent with "base Agda", and it was weird to fix one but not both;

• If a data type is accepted under some flags, then its eliminator/recursor should also be accepted, without any extra flags.

So the revert sounds okay for now.