Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_78b30553736394a539413931fa1cff2bc3bf0593f21193fd84994ec92c37add8 with
λ x3 x4 : ι → ι → ι . In x2 (x4 x0 x1).
Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with
x0,
Sing x1,
x2.
The subproof is completed by applying H0.