exact hmotive rfl
case h
α : Type u_1
β : Type u_2
motive : Prop
L : List α
f : (L_1 : List α) → ↑L_1 = ⟦L⟧ → β
h : ∀ (a b : List α) (ha : ↑a = ⟦L⟧) (hb : ↑b = ⟦L⟧), f a ha = f b hb
hmotive : ∀ {L_1 : List α} {hL : ↑L_1 = ⟦L⟧}, elim ⟦L⟧ f h = f L_1 hL → motive
⊢ motive
no goals