bug.jonprl

Theorem foo : [(n : nat) -> (x : =(zero; succ(n); nat)) -> =(zero; succ(n); nat)] {
  intro; aux {auto};
  intro; aux {auto};
  hypothesis #2  ||| works just fine here
}.

Operator is-zero : (0).
[is-zero(n)] =def= [natrec(n; unit; _._. void)].

Theorem succ-not-zero : [(n : nat) -> =(succ(n); zero; nat) -> void] {
  auto;
  assert [is-zero(succ(n))]; 
  aux { 
    unfold <is-zero>;
    subst [=(succ(n); zero; nat)] [h. natrec(h; _; _._. _)]; auto; 
    aux { hypothesis #2 };  ||| fails with seemingly identical sequent here
    reduce; auto
  };
  unfold <is-zero>; reduce; auto
}.