∀ {α : Type u} {β : α → Type v} {motive : List ((a : α) × β a) → Prop},
  motive [] →
    (∀ (k : α) (v : β k) (tail : List ((a : α) × β a)), motive tail → motive (⟨k, v⟩ :: tail)) →
      ∀ (t : List ((a : α) × β a)), motive t