Let x0 of type ι be given.
Apply unknownprop_8caab58746e5d2d24e79c56b1fd1ad38271bed0128653f24088edadc36aa9114 with
x0,
λ x1 x2 . f6a32.. x1 = 4a7ef...
Apply unknownprop_23664dbeb9b115697e6a9c597ef741d81e66962cba0c9c5f51bdcd68c09e293f with
x0,
4a7ef.. leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_a66a65189a5389c2141d18df52f52fcf5f074fba68040a0bda3b8b81c830611a.