equation compiler failed to prove equation lemma

Stream: new members

[Horatiu Cheval]

Sorry for the long example, I didn't manage to further isolate the problem.
I get equation compiler failed to prove equation lemma when defining match_lcase, but I don't see what's wrong with this recursion. What's happening?

inductive type
| zero : type
| comp : type → type → type

infixr `>>` : 50 := type.comp

inductive var (τ : type)
| mk : ℕ → var

inductive term : type → Type
| app : ∀ {τ σ : type}, term (σ.comp τ) → term σ → term τ
| const : ∀ {τ : type}, term τ
| S : ∀ {ρ τ σ : type}, term $ (τ >> σ >> ρ) >> (τ >> σ) >> τ >> ρ

open term
inductive lcase : ∀ {σ τ : type}, var σ → term τ → Type
| mk_const : ∀ {σ τ : type} {x : var σ} {t : term τ}, lcase x t
| mk_app : ∀ {ρ σ τ : type} {x : var ρ} {u : term (σ.comp τ)} {v : term σ},
    lcase x u → lcase x v → lcase x (u.app v)

@[simp]
def match_lcase : ∀ {σ τ : type} {x : var σ} {t : term τ}, lcase x t → term (σ >> τ)
| σ τ x t (lcase.mk_const) := @const (σ >> τ)
| σ τ x t (lcase.mk_app lu lv) := (S.app $ match_lcase lu).app $ match_lcase lv