Re: [isabelle] Unifiction question
To do that, you need to show somehow that "a" equals one of the
arguments of ?V_ff32. You say its arguments include "a Un a", but I
see "a Un aa". If indeed a = nV_f2 - aa then "a" and "aa" are
disjoint, so "a Un aa" can't equal "a".
On 10 Nov 2005, at 21:09, shimonyb at techunix.technion.ac.il wrote:
My question: Is it possible to unify the premisis and the subgoal,
using the additional assumption i have: 'a = nV_f2 - aa' ?
This archive was generated by a fusion of
Pipermail (Mailman edition) and