Generalize apply to the no forall case

Fixes #27
The (all) cookie on unfold now keeps all solutions in a disjunct

Fixes #30
Single unfold case inadvertently omitted in previous commit
Allow variable renaming to override instantiated variables
Complain about invalid bound or declared identifiers
More stringent checks on identifiers
Resolving the extra shift/reduce conflict introduced with checked ids
unfold (all) needs to do a deep copy of the term per disjunct

Here's the basic issue:

    Kind i type.
    Type c, d i.

    Define p : i -> prop by
      p X := X = c
    ; p X := X = d.

    Theorem foo : forall X, p X.
    intros. unfold (all).

Without a deep copy, one would get the subgoal:

    ==========================
     ?1 = c \/ X = d

because in order to construct the second disjunct the binding
state would have been reset.
Fixing deep copying of terms in previous commit

Turns out that one cannot head-normalize during a deep copy
since that might prevent the binding state from being undone.
Updating changelog
Also allow backchain to clear its argument
Fix yet another build error on 3.12.1