Apply In_ind with
λ x0 . nIn x0 (V_ x0).
Let x0 of type ι be given.
Assume H0:
∀ x1 . x1 ∈ x0 ⟶ nIn x1 (V_ x1).
Apply V_E with
x0,
x0,
False leaving 2 subgoals.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H2: x1 ∈ x0.
Apply H0 with
x1 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply H3 with
x1.
The subproof is completed by applying H2.