Apply unknownprop_4c4b27a97d7f3e81d4abb7629b850d6c55c186f55f30e3dfae132a3ddf1e0a30 with
4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))),
4a7ef...
The subproof is completed by applying unknownprop_65971d7fb82cf658cabe1adc2decc738c44e6424e0df2d626e88c5c4d2ad7ccb.