∀ {ι : Type u_1} {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)}
  (motive : (l : List ι) → ((i : ι) → i ∈ l → Quotient (S i)) → Sort u_3) (i : ι) (tail : List ι)
  (q : (i_1 : ι) → i_1 ∈ i :: tail → Quotient (S i_1)) (h_1 : (q : (i : ι) → i ∈ [] → Quotient (S i)) → motive [] q)
  (h_2 : (i : ι) → (tail : List ι) → (q : (i_1 : ι) → i_1 ∈ i :: tail → Quotient (S i_1)) → motive (i :: tail) q),
  (match i :: tail, q with
    | [], q => h_1 q
    | i :: tail, q => h_2 i tail q) =
    h_2 i tail q