# [isabelle] A quick question about fixing variables in a proof

Hi,
I'm trying to just fix a functional variable in a proof as follows:
typedecl S
typedecl T
consts
G :: "S * T => real"
s :: T
f :: T
locale A =
fixes p :: Obj
assumes cons: "!! t1 t2. G(p,t1) = G(p,t2)"
locale B =
...
lemma A_B_inconsistent:
assumes "A p"
shows "False"
proof -
fix func
interpret localA: A p
by fact
interpret localB: B p
by fact
show "False"
proof -
have "func(p,s) = func(p,f)"
using localA.cons
by auto
qed
next
...

`Does anyone know how to unify 'func' to G and s/f to the second argument?
``Why can't auto unify them?
`
Any help will be much appreciated.
Thank you
John

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