∀ {α : Type u_1} (motive : (σs : List (Type u_1)) → (Std.Do.SVal.StateTuple σs → α) → Sort u_2) (head : Type u_1)
  (tail : List (Type u_1)) (f : Std.Do.SVal.StateTuple (head :: tail) → α)
  (h_1 : (f : Std.Do.SVal.StateTuple [] → α) → motive [] f)
  (h_2 :
    (head : Type u_1) →
      (tail : List (Type u_1)) → (f : Std.Do.SVal.StateTuple (head :: tail) → α) → motive (head :: tail) f),
  (match head :: tail, f with
    | [], f => h_1 f
    | head :: tail, f => h_2 head tail f) =
    h_2 head tail f