(motive : (x x_1 : Fin 2) → x ≤ x_1 → Sort u_1) →
  (x x_1 : Fin 2) →
    (x_2 : x ≤ x_1) →
      ((isLt isLt_1 : 0 < 2) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_1⟩ x) →
        ((isLt : 0 < 2) → (isLt_1 : 1 < 2) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_1⟩ x) →
          ((isLt isLt_1 : 1 < 2) → (x : ⟨1, isLt⟩ ≤ ⟨1, isLt_1⟩) → motive ⟨1, isLt⟩ ⟨1, isLt_1⟩ x) → motive x x_1 x_2