(head : Type u_1) →
  (tail : List (Type u_1)) →
    (motive : Std.Do.SVal.StateTuple (head :: tail) → Sort u_2) →
      (x : Std.Do.SVal.StateTuple (head :: tail)) →
        ((s : head) → (t : Std.Do.SVal.StateTuple tail) → motive (s, t)) → motive x