Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 8 / a / i / Solution

Apply the negation introduction rule to an assumed existential statement and the existential quantifier elimination rule with a fresh witness $u$:The eigenvariable condition holds: $u$ is absent from the surrounding premise, the existential assumption and the exported conclusion $\perp$. Its local assumption is discharged before the final negation introduction rule.