Let x0 of type ι be given.
Apply unknownprop_8bd7560a9991903264b52a55534d2167a6f1ceb54602573e16d8e12432ce96be with
λ x1 . In x1 0,
x0.
The subproof is completed by applying H0.
Apply notE with
∃ x1 . In x1 0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_641980b1f679699e58af9b75e8660e324a5a8b56d6549ff9c993636d65c0d9dc.
The subproof is completed by applying L1.