Let x0 of type ι be given.
Apply unknownprop_694898c9791aec4140fc01c2b4287388fd1297142d7e1ee2585d4a7ba4f43dce with
λ x1 x2 : ι → ο . x2 x0.
Apply unknownprop_92b4103b83752522eb6c235601eefa2912e3f6395a346e3a7eb52bb5e37ede81 with
x0.
The subproof is completed by applying H0.