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.