Propositional irrelevance confusion

Stream: lean4

[Jad Ghalayini]

So I've been working on a lean development where I wanted to rewrite using a lemma of the form

Hei : Stlc.HasType.interp (_ : Context.stlc Γ⊧Term.stlc e (Context.sparsity Γ):Ty.coprod (Term.stlc_ty A) (Term.stlc_ty B))
    (Stlc.Context.interp.downgrade G) =
  ei

Alas,

 rw [Hei] at Ie'

doesn't work, but

rw [Stlc.HasType.interp_irrel] at Ie'
rw [Hei] at Ie'

does, where we have

theorem Stlc.HasType.interp_irrel
  (H: Γ ⊧ a: A)
  (H': Γ ⊧ a: A)
  : H.interp = H'.interp
  := rfl

I realized this was probably an issue, since propositional irrelevance usually holds, but trying to minimize the issue, all I could come up with, namely

inductive SquashBool: Prop
| truthy
| falsy

def not': Bool -> SquashBool -> Bool
| true, _ => false
| false, _ => true

theorem not'_irrel: not' b s = not' b s' := rfl

theorem not'_not': not' (not' b falsy) truthy = b
:= by {
  cases b <;> rfl
}

theorem not'_not'': not' (not' b truthy) falsy = b
:= by rw [not'_not']

inductive NonZero: Nat -> Prop
| succ: NonZero (n + 1)
| succ': NonZero (n + 1)

theorem nonzero_mk: m = n + 1 -> NonZero m := by {
  intro H;
  rw [H]
  constructor
}

def safe_pred: (n: Nat) -> NonZero n -> Nat
| 0, p => False.elim (by cases p)
| n + 1, _ => n

theorem safe_pred_irrel: safe_pred n p = safe_pred n p' := rfl

theorem safe_pred_succ
 (H: m = n + 1):
 (safe_pred m (nonzero_mk H)).succ = m := by {
   cases m with
   | zero => cases H
   | succ m => rfl
 }

 theorem safe_pred_succ':
  (safe_pred m p).succ = m := by {
    rw [safe_pred_succ]
    repeat sorry
  }

works just fine, and so I'm confused as to how to even go about minimizing this. I'm pretty confident it's a bug though, but who knows.