∀ {ι : 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 t : Set ι}
  (e : InverseSystem.PEquivOn f equivSucc t) (h : s ⊆ t) (i : ↑s), (e.restrict h).equiv i = e.equiv ⟨↑i, ⋯⟩