Confusing behavior with `solve_by_elim`

Stream: general

[Nico Lehmann]

I have the following goal

a✝² : Vname
a✝¹ a✝ : LExp
ih1 : ∀ {s : State} {n : Val}, lval a✝¹ s = n → LvRel s a✝¹ n
ih2 : ∀ {s : State} {n : Val}, lval a✝ s = n → LvRel s a✝ n
s : State
⊢ LvRel s (llet a✝² a✝¹ a✝) (lval (llet a✝² a✝¹ a✝) s)

which is solved by

    constructor
    · solve_by_elim
    · solve_by_elim

I'm confused about why solve_by_elim doesn't solve the entire goal. I thought solve_by_elim uses constructor if no lemma applies. Why could that be?

[Nico Lehmann]

The goal is solved if I pass the constructor solve_by_elim [LvRel.lvRelL]

This is the definition of LvRel

inductive LvRel : State -> LExp -> Val -> Prop where
| lvRelN : ∀ {s: State} {n: Val},
              LvRel s (num n) n
| lvRelV : ∀ {s: State} {x: Vname},
              LvRel s (var x) (s x)
| lvRelP : ∀ {s: State} {e1 e2 : LExp} {n1 n2 : Val},
              LvRel s e1 n1 -> LvRel s e2 n2 ->
              LvRel s (plus e1 e2) (n1 + n2)
| lvRelL : ∀ {s: State} {x: Vname} {e1 e2: LExp} {n1 n2: Val},
              LvRel s e1 n1 -> LvRel (s [x := n1]) e2 n2 ->
              LvRel s (llet x e1 e2) n2

[Nico Lehmann]

No ideas?

[Kevin Buzzard]

#mwe ?