Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_fc3f08095f77ec388b89b48e2b52040a80a894c58ae8421f993dbbc015fb91c5 with
λ x2 x3 : ι → ι → ι . ∀ x4 . In x4 x0 ⟶ In (Inj0 x4) (x3 x0 x1).
The subproof is completed by applying unknownprop_1fbfebc9584f3b35fe974f93c7762fab1d5a4f649af5608ad307cbbc36ce4d37 with
x0,
Power x1.