Let x0 of type ι be given.
Apply unknownprop_4be0565ac5b41f138f7a30d0a9f34a5d126bb341d2eeaa545aa7f0c1552b9722 with
0,
x0,
λ x1 x2 . x2 = 0 leaving 3 subgoals.
The subproof is completed by applying unknownprop_85a866d410bbf26b260c37246259122da00d151df84a9a2a98da7e65f3fcf36a.
The subproof is completed by applying H0.
Apply unknownprop_125482bd1feb67ec2e9da6790eb6492e3ac6b5310e309d7023b9247b76e919b5 with
x0.
The subproof is completed by applying H0.