WellFounded
  (invImage
      (fun x =>
        PSum.casesOn x (fun _x => PSigma.casesOn _x fun e offset => (sizeOf e, 1)) fun _x =>
          PSigma.casesOn _x fun e offset => (sizeOf e, 0))
      Prod.instWellFoundedRelation).1