[isabelle] schematic variables and assumption
I have the following lemma:
lemma "(¬ (∀ x . P x)) ⟹ (∃ x . ¬ P x)"
apply (rule exI)
apply (rule notI)
apply (erule notE)
apply (rule allI)
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and