Harpoon removes a substitution variable from the scope when splitting on a variable using the substitution

[Ailrun]

The last theorem of f7d0d7a, namely

anti-renameSN
{g : cxt} {g' : cxt} {$R : [g' |-# g]} {M : [g |- tm A[]]} SN [g' |- M[$R]] -> SN [g |- M]

shows the problem.

When splitting on a variable whose type is SNRed' [g' |- $R[..]] [g |- M] [g' |- N[$R[..]]], the substitution variable $R goes out of the scope and it is not possible to use it inside of the necessary command

solve SRed x3 (anti-renameSN [g] [g'] [g' |- $R] [g |- N] x2)

Also, it is not possible to use _ instead of $R since the syntax is not allowed for substitution variables.

[Ailrun]

Workaround: convert constructors of SNRed' type to use only explicit meta-variables.

[Ailrun]

FYI: This is an intended behavior but I think it would be great if it is possible to ameliorate this restriction.