# [isabelle] What is the error (simp)?

The following lemma fails to verify (in ZF). It is strange because (simp) should do the job.
lemma comp_eq_id_iff2:
"[| g: B->Ag; f: Af->C; Ag<=Af |] ==> (ALL y:B. f`(g`y) = y) <-> f O g = id(B)"
proof -
assume "g: B->Ag" "f: Af->C" "Ag<=Af"
hence "f O g: B->C" by (rule comp_fun2)
moreover
have "id(B): B->B" by (rule id_type)
ultimately have m: "(ALL y:B. (f O g)`y = id(B)`y) <-> f O g = id(B)" by (rule fun_extension_iff)
from `g: B->Ag` have c [simp]: "y:B ==> (f O g)`y = f`(g`y)" by auto
have i [simp]: "y:B ==> id(B)`y = y" by auto
from m show "(ALL y:B. f`(g`y) = y) <-> f O g = id(B)" by simp
qed
What is my error? What is the right way to do this?
--
Victor Porton - http://portonvictor.org

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