Guard against partial applications of wfrec functions (closes #555, #609)

[blume0]

Fixes #555, fixes #609.
The function Covering.add_wfrec_implicits adds a hole at the end of every well-founded recursive function call ( corresponding to the proof that the call is decreasing), and does not check if the call has enough arguments.
This PR adds a check that the function is fully applied, and reports an error to the user otherwise.

PS
An alternative would be to eta-expand such partial applications inorded to be able to insert the wfrec hole, howerer, this might abstract away information needed for the wfrec proof and result in confusing unsolvable obligations. For example, with this alternative, while it would allow this definition

Equations plus (n : nat) (m : nat) : nat by wf n lt :=
  plus 0 m := 0;
  plus (S n) m := S (let plus_n := plus n in plus_n m).

to pass, if one tries

Equations plus (n : nat) (m : nat) : nat by wf n lt :=
  plus 0 m := 0
  plus (S n) m := S (let plus' := plus in plus' n m

it succeeds but leaves an obligation of the form n0 : nat |- n0 < S n with no information about n0.
A realistic example where this second case occurs is the last definition with manual eta-expansion in #609.