# [isabelle] Proving equivalence

Hi all,
I'm having problem proving the following. Say I have:
axiomatization
foo :: "real => real => real" and
bar :: "real => real => real" and
bax :: "real => real => real"
where ax1: "ALL p r v e. (r = foo p e & v = bar p e) = (bax r e = v)"
lemma "ALL p r v e. bax r e = bar p e"
using ax1
by auto
The lemma can be proved. However, if I change the signature of bax to "real
=> real => real => real":
axiomatization
foo :: "real => real => real" and
bar :: "real => real => real" and
bax :: "real => real => real => real"
where ax2: "ALL q p r v e. (r = foo p e & v = bar p e) = (bax q r e = v)"
lemma "ALL q p r v e. bax q r e = bar p e"
using ax2
by auto
Auto can't find a proof. How come this is so difficult for auto? What is the
proper way to do this proof?
Thanks
Steve

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