{ι : Type u_6} →
  {F : ι → Type u_7} →
    {X : ι → Type u_8} →
      [inst : LinearOrder ι] →
        {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} →
          [inst_1 : SuccOrder ι] →
            {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} →
              {s : Set ι} → InverseSystem.PEquivOn f equivSucc s → (i : ↑s) → F ↑i ≃ InverseSystem.piLT X ↑i