Apply H0 with
4ae4a.. (4ae4a.. 4a7ef..),
4a7ef.. leaving 2 subgoals.
The subproof is completed by applying unknownprop_c6d721b795faf1c324094ad380dfe62a3a5dc2ef0b2edf42237be188f6768728 with
4ae4a.. (4ae4a.. 4a7ef..).
The subproof is completed by applying unknownprop_94c438c3f41134cd86e0be06a85b5e5b3aa8448f9221f51d2dfe9b1364042f49.
Apply unknownprop_cda77d97aaeddfc93c22dbfd5eb7b2f0f0565ebd4bc09571f536213e70c0ca50.
Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with
4ae4a.. (4ae4a.. 4a7ef..),
4a7ef...
The subproof is completed by applying L1.