Apply unknownprop_397dcfaa62ddf41d498e7fd580ff4a854ed9ebd3c9ab727b2b23fe272ecb1aa4 with
4ae4a.. 4a7ef..,
4a7ef.. leaving 2 subgoals.
The subproof is completed by applying unknownprop_694af00b5a127570fee7483dc305b7382527fa7c05e199a9b8a45bebf6738362.
The subproof is completed by applying unknownprop_375af585d676cd889234cd20860ce45033e1ffceb375ac6277c1b1a2e16f15bd.