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