Apply unknownprop_ce9033a67ef84c6ab0b67c7e947b752573b6048f7ffe5e81030bc8cffa5f9d29 with
4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))),
4ae4a.. 4a7ef...
The subproof is completed by applying unknownprop_ac927f2ad247eb36bc322e3579f4429fc5e423f90a2de7867227e2cfdd51eb3e.