theory A
imports Main
begin

definition foo where "foo x = x"

lemma a: "foo (foo x) = x" unfolding foo_def ..
 
end