Let x0 of type ι be given.
Apply unknownprop_b67f6d586fb9d8883c38540f89ba210beeb3fabc8048f066af6580d3cbff51ec with
4ae4a.. x0.
Apply unknownprop_11171438c9340577bc5ca6838eccea0ebdb4279227053bf618ee42741f7851b4 with
x0.
Apply unknownprop_03f5f7248b8d06fe27b9a4f75f4e437d5e9b43a9092733e8b3f6dcfe61f5e308 with
x0.
The subproof is completed by applying H0.