# [isabelle] Unifiction question

Hi,
In the following formula, I have reahced a state where the assumptions includes
the schemtic variable: ?V_ff32 which has several arguments among them: '(a Un
a)', while the subgoal includes a term with only 'a' as one of its arguments:
!!. n_e n_evs nV_f1 nE_f1 nV_f2 nE_f2 v1 v1a v2 v2a a b aa ba.
[| .... ; nV_f1 Int ?V_ff32 {v1, v2} n_evs nV_f1 nE_f1 (a Un
aa)(insert {v1, v2} (b Un ba)) = {}|]
==> nV_f1 Int a = {}
My question: Is it possible to unify the premisis and the subgoal, possibly
using the additional assumption i have: 'a = nV_f2 - aa' ?
Thanks

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