Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0:
ap x0 x1 = x2.
Assume H1: x2 = 0 ⟶ ∀ x3 : ο . x3.
Assume H2: x0 = 0.
Apply H1.
Apply H0 with
λ x3 x4 . x3 = 0.
Apply H2 with
λ x3 x4 . ap x4 x1 = 0.
The subproof is completed by applying ap_const_0 with x1.