LEAN4 Termination Error

There seems to be an unresolvable error when LEAN4 tries to typecheck the following code and tries to prove termination of "pairLeftRecursor" function here. Removing the comment at the end causes the kernel to panic.

inductive EX {A : Type} (P : A → Type) : Type
  | intro (w : A) (h : P w)

inductive EQ {A : Type} : A → A → Type
  | refl (r : A) : EQ r r

inductive Term : Type
  | pair (t1 t2 : Term)

def Set A := A -> Prop

abbrev TermSet := Set Term

inductive dy : TermSet → Term → Type
  | something {x y} : dy x y

inductive Assertion : Type
  | eq (t u : Term)
  | member (t₀ : Term) (tlist : List Term)

abbrev AssertionSet := Set Assertion

mutual
inductive eq_ady : TermSet → AssertionSet → Assertion → Type
  | cons_pair {S : TermSet} {A : AssertionSet} {t1 t2 u1 u2 : Term} (p1 : eq_ady S A (Assertion.eq t1 u1)) (p2 : eq_ady S A (Assertion.eq t2 u2)) : eq_ady S A (Assertion.eq (Term.pair t1 t2) (Term.pair u1 u2))
  | irrelevant {S A B} : eq_ady S A B
inductive Eq_Trans : TermSet → AssertionSet → Term → Term → Type
  | two_trans {S : TermSet} {A : AssertionSet} {t1 t2 t3 : Term} (p1 : eq_ady S A (Assertion.eq t1 t2)) (p2 : eq_ady S A (Assertion.eq t2 t3)) : Eq_Trans S A t1 t3
  | trans_trans {S : TermSet} {A : AssertionSet} {t1 tk tk' : Term} (phead : eq_ady S A (Assertion.eq t1 tk)) (plist : Eq_Trans S A tk tk') : Eq_Trans S A t1 tk'
end

def pairLeftRecursor {S A t u} : Eq_Trans S A t u →
        Option (
          (EX fun t1  => EX fun x1 => EX fun x2 =>
              eq_ady S A (Assertion.eq t1 x1) × (eq_ady S A (Assertion.eq (x1.pair x2) u)) × (EX fun t2 => EQ t (t1.pair t2)))
        ) := by
  intros p
  cases p with
  | @two_trans _ x _ p1 p2 => apply Option.none
  | trans_trans phead plist =>
    match phead with
    | @eq_ady.cons_pair _ _ t1 t2 x1 x2 a b => apply Option.none
    | phead =>
      match (pairLeftRecursor plist) with
      | Option.none => apply Option.none
      | Option.some p => apply Option.no
  -- decreasing_by (all_goals sorry)

This issue was first discussed in the Zulip here, and was encountered in the formalisation of this paper.

To reproduce, just copy paste the above code into https://live.lean-lang.org/. (The error also occurs on the nightly version). Tried on latest Mathlib version and latest nightly version as of today.

Reproduce the termination error by copying the issue's code into https://live.lean-lang.org/, including the commented decreasing_by line, and compare the behavior with the nightly version. Read the linked Zulip discussion for existing context. Done means the example typechecks without an unresolvable termination error or kernel panic.