page 1  1 2 3 4 
We want to prove
( L : List N : Nat ) N in nil = falseConjunction elimination yields 2 subgoals:
And thus the main goal is proved. 
Explanation
This is a straightforward verification of the two axioms in the specification BASICSET : conjunction elimination turns the goal into the two
equations, which are then easily checked by reduction in the theory of lists.

