[isabelle] Novice question about functions

I am writing my first real Isabelle theory (indeed very useful for other Isabelle users). I step on the following question.
Let move_fun is an arbitrary function and myset is an arbitrary set (in ZF). How to prove the theorem (marked sorry)?
theory test
  imports ZF

locale subtest =
  fixes move_fun::"i=>i"
  fixes myset::i

definition "move == (lam x:myset. move_fun(x))"

theorem "x: my_set ==> move`x = move_fun(x)" sorry


Victor Porton - http://portonvictor.org

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.