# Re: [isabelle] schematic variables and assumption

Such a step would not be sound. You can only unify ?x with terms containing no bound variables. Variable capture is never allowed.
Your example is quite tricky to prove in a natural deduction calculus. Of course, it's trivial if you use automation.
Larry Paulson
On 15 May 2012, at 12:31, Viorel Preoteasa wrote:
> Hello,
>
> I have the following lemma:
>
> lemma "(¬ (∀ x . P x)) ⟹ (∃ x . ¬ P x)"
> apply (rule exI)
> apply (rule notI)
> apply (erule notE)
> apply (rule allI)
> apply assumption
>
> After the the rule "apply (rule allI)" the goal becomes:
> ⋀x. P ?x ⟹ P x
>
> I do not understand why "apply assumption" fail at this point.
> I would expect that ?x is unified with x and the proof succeed.
>
> Best regards,
>
> Viorel Preoteasa
>

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