[isabelle] Unifiction question


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' ?


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