Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_fc3f08095f77ec388b89b48e2b52040a80a894c58ae8421f993dbbc015fb91c5 with
λ x3 x4 : ι → ι → ι . In (Inj1 x2) (x4 x0 x1).
Apply unknownprop_509aadde20bd8e655e679e36fea278577d08a1dbe475eed73f3fccc8c2d65f15 with
x0,
Power x1,
x2.
Apply unknownprop_9a40b4678ae1931e61346f9ab9e405ec760f2f9d44b3be548b52a8b2ddb78559 with
x1,
x2.
The subproof is completed by applying H0.