Inverting twice makes a meta-context variable become in scope

[MartyO256]

Loading this signature in Harpoon:

LF nat : type =
| zero : nat
| succ : nat -> nat
;
--name nat N.

LF lt : nat -> nat -> type =
| lt/z : lt zero (succ N)
| lt/s : lt N1 N2 -> lt (succ N1) (succ N2)
;

LF location : type =
| location/i : nat -> location
;

LF loc-lt : location -> location -> type =
| loc-lt/i : lt N N' -> loc-lt (location/i N) (location/i N')
;

LF loc-succ : location -> location -> type =
| loc-succ/i : loc-succ (location/i N) (location/i (succ N))
;

proof lt-succ : { N : [|- nat] } [ |- lt N (succ N)] =
/ total 1 /
intros
{ N : ( |- nat)
|
; split [ |- N] as
  case succ:
  { N1 : ( |- nat)
  |
  ; by lt-succ [ |- N1] as L unboxed;
    solve [ |- lt/s L]
  }
  case zero:
  {
  |
  ; solve [ |- lt/z ]
  }
}
;

proof loc-succ-lt : [ |- loc-succ L L'] -> [ |- loc-lt L L'] =
/ total /
?
;

loc-succ-lt can be incorrectly proven using

invert x
invert x
by lt-succ [ |- N] as Q unboxed
solve [|- loc-lt/i Q]

which produces the program

  fn y =>
  let [ |- loc-succ/i ] = y in
  let [ |- loc-succ/i ] = y in
  let [ |- Q] = lt-succ [ |- N] in [ |- loc-lt/i Q]

After the first invert x, the meta-context variable N : ( |- nat) is not in scope.
It becomes in scope after the second invert x, which is why it can be accessed directly in by lt-succ [ |- N] as Q unboxed.

For any x, it should not be possible to perform a case analysis for x while being in a case analysis for x.