Using the lambdasubst hack-- instead of formulating lemmas for (App e1 v), formulate them for (e1[x:=v]).