∀ {ι : Type u_1} {F : ι → Type u_2} {X : ι → Type u_3} {i : ι} [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} [WellFoundedLT ι]
  (e : (j : ↑(Set.Iio i)) → InverseSystem.PEquivOn f equivSucc (Set.Iic ↑j)) (x x_1 : ↑(Set.Iio i)) (h : ↑x ≤ ↑x_1),
  InverseSystem.piLTProj h ((e x_1).restrict ⋯).equiv = ((e x).restrict ⋯).equiv