Apply unknownprop_397dcfaa62ddf41d498e7fd580ff4a854ed9ebd3c9ab727b2b23fe272ecb1aa4 with
4ae4a.. (4ae4a.. 4a7ef..),
4ae4a.. 4a7ef.. leaving 2 subgoals.
The subproof is completed by applying unknownprop_b67d0b5e367b954e6f4bf572a13703ac003fabf78495386b4de466972529effb.
The subproof is completed by applying unknownprop_e256c3837ff221325e66d4c83283618d462d76cb96bca463e1abd4876bf63511.