{ι : Type u_1} →
  [inst : Preorder ι] →
    {F : ι → Type u_4} →
      {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} →
        {motive : InverseSystem f → Sort u} →
          ((map_self : ∀ ⦃i : ι⦄ (x : F i), f ⋯ x = x) →
              (map_map : ∀ ⦃k j i : ι⦄ (hkj : k ≤ j) (hji : j ≤ i) (x : F i), f hkj (f hji x) = f ⋯ x) → motive ⋯) →
            (t : InverseSystem f) → motive t