apply tactic fails to do equivariant matching

[chaudhuri]

This should work, but doesn't.

Kind i type.
Type p i -> prop.

Theorem bad : nabla x y, (p x -> false) -> (p y -> false).
intros. apply H1 to H2.

To make it work we need this proof.

Theorem works : nabla x y, (p x -> false) -> (p y -> false).
intros.
assert forall (z:i), nabla x, p x -> false.
apply H3 to H2.

Alternatively, use backchain instead of assert and apply.

The reason for the forall for the asserted formula there is an unrelated bug to be filed presently.

[chaudhuri]

See also #27.

[chaudhuri]

This is probably ultimately not a bug at all, since the permute tactic can be used to renumber the nominals. It makes the scripts a bit more manual than one would like, perhaps.