Apply H0 with
4ae4a.. 4a7ef..,
4a7ef.. leaving 2 subgoals.
The subproof is completed by applying unknownprop_c6d721b795faf1c324094ad380dfe62a3a5dc2ef0b2edf42237be188f6768728 with
4ae4a.. 4a7ef...
The subproof is completed by applying unknownprop_375af585d676cd889234cd20860ce45033e1ffceb375ac6277c1b1a2e16f15bd.
Apply unknownprop_71b93dd42392a89c7d0d83acd26ffcfa49cbfca42eafcbc1c9a23dfe9597ebbf.
Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with
4ae4a.. 4a7ef..,
4a7ef...
The subproof is completed by applying L1.