Apply unknownprop_23664dbeb9b115697e6a9c597ef741d81e66962cba0c9c5f51bdcd68c09e293f with
4a7ef..,
4ae4a.. 4a7ef.. leaving 2 subgoals.
The subproof is completed by applying unknownprop_a66a65189a5389c2141d18df52f52fcf5f074fba68040a0bda3b8b81c830611a.
The subproof is completed by applying unknownprop_3d71b8748f06c73392acc73d46c8ae7fc07e5709a18169240b1cb765b8547148.