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