Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Apply H0 with
explicit_Group x0 x1.
Apply unknownprop_6881ac7ad4356c09fff02e0a39d3a1d9923586474092567f0c58da443f0e8918 with
x0,
x1,
λ x2 x3 : ο . x2.
The subproof is completed by applying H2.