Let x0 of type ι be given.
Apply unknownprop_34004d936e9c770d7776a68f4fd89de16dd752c63a364055547f1f2fd867c6b6 with
4ae4a.. (e4431.. x0),
45abd.. x0 leaving 2 subgoals.
Apply unknownprop_1f03c3e4cc230143731a84d6351b78522f6051d5113f644774435abf9cb5a984 with
e4431.. x0.
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_c34124601e2e06130efa5354260ddd535b67908e8c12e7d9d87ccfe50027c7c6 with
x0.
The subproof is completed by applying H0.