{Γ : Type u_1} →
  {R : Type u_2} →
    [inst : PartialOrder Γ] →
      [inst_1 : Zero R] →
        {motive : HahnSeries Γ R → Sort u} →
          (t : HahnSeries Γ R) →
            ((coeff : Γ → R) →
                (isPWO_support' : (Function.support coeff).IsPWO) →
                  motive { coeff := coeff, isPWO_support' := isPWO_support' }) →
              motive t