Let x0 of type ι be given.
Apply unknownprop_443bf25288cf39bc78395680f7fe50ad1a2a509c594b439821412f6af4f99866 with
x0,
4a7ef..,
λ x1 x2 . x2 = x0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_a66a65189a5389c2141d18df52f52fcf5f074fba68040a0bda3b8b81c830611a.
Apply unknownprop_ccff4249496414413c3c95467fb8c02c96509ca2826dc03833e7de26e75fcd74 with
x0.
The subproof is completed by applying H0.