Variable capture in unfolding definitions

[chaudhuri]

Consider the following Abella theory:

Kind p type.

Type one,up p -> p -> prop.

Define bup : p -> prop by
  bup Q :=
    exists Q1, one Q Q1 /\ exists Q2, up Q1 Q2.

Theorem foo : forall Q1 (Q2:p), bup Q1 -> false.
intros. case H1.

The final line produces: H2 : up Q3 Q3, which is invalid. Since both Q1 and Q2 are exists-bound, the new hypothesis should have different arguments to up.

[chaudhuri]

This bug is reported by @matteocimini.