NO

Problem:
 fapp(lam(X),Y) -> subst(X,Y)
 subst(v(),Y) -> Y
 subst(lam(X),Y) -> lam(X)
 subst(fapp(X,Z),Y) -> fapp(subst(X,Y),subst(Z,Y))

Proof:
 Unfolding Processor:
  loop length: 4
  terms:
   fapp(subst(v(),lam(fapp(v(),v()))),lam(fapp(v(),v())))
   fapp(lam(fapp(v(),v())),lam(fapp(v(),v())))
   subst(fapp(v(),v()),lam(fapp(v(),v())))
   fapp(subst(v(),lam(fapp(v(),v()))),subst(v(),lam(fapp(v(),v()))))
  context: []
  substitution:
   
  Qed