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