Split: Variable renaming required

[wikku]

Kind t type.

Theorem fine :
    (forall (B : t), B = B) ->
    (forall (A : t), A = A) /\
    (forall (A : t), A = A).
  intros. split. search. search.

Split fine as fine1, fine2.

Theorem bad :
    (forall (A : t), A = A) ->
    (forall (A : t), A = A) /\
    (forall (A : t), A = A).
  intros. split. search. search.

Split bad as bad1, bad2.

[ABELLA BUG]
Variable renaming required
Please report this at  https://github.com/abella-prover/abella/issues
Error: Bug

The same happens with nabla variables.

[chaudhuri]

The Split command is being way too aggressive in preventing theorems like: forall A, (forall A, A = A) -> A = A. This exact theorem can be stated manually by the user with no issues.