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