{ι : Type u_1} →
  {motive : ComplexShape ι → Sort u} →
    ((Rel : ι → ι → Prop) →
        (next_eq : ∀ {i j j' : ι}, Rel i j → Rel i j' → j = j') →
          (prev_eq : ∀ {i i' j : ι}, Rel i j → Rel i' j → i = i') →
            motive { Rel := Rel, next_eq := next_eq, prev_eq := prev_eq }) →
      (t : ComplexShape ι) → motive t