Let x0 of type ι be given.
Apply unknownprop_18724cb817cb481b8967b1efe13d39d42daa75ec771890da7ad3a6b6981daf0e with
1216a.. (b5c9f.. x0 x0) (λ x1 . bij x0 x0 (λ x2 . f482f.. x1 x2)),
λ x1 x2 . 0fc90.. x0 (λ x3 . f482f.. x2 (f482f.. x1 x3)).
The subproof is completed by applying unknownprop_bc372826b7f0da52f3a8a3ea86862b41fc91267615627787d3fb4a389b8c72dc with x0.