Apply unknownprop_026e367f8c98c27bd0f571461f5fabafe5e3a793ffb10b9778df109026991f65 with
8dd2c..,
c6963..,
a9894..,
da724..,
adebb..,
91922.. leaving 11 subgoals.
The subproof is completed by applying unknownprop_14a4ee8538d143fe8dc45eb2eb967d12f82b99130422357962aa2d0a55ab88f9.
The subproof is completed by applying unknownprop_57b8ec8100fb47d95fd7bcee1eb4fed21bcf07a9bbfc00cf18bdb9c88823060f.
The subproof is completed by applying unknownprop_61bcd948d8df9a37b038fa76c8759a4ad7ce26206212c492a4e81a8500373590.
The subproof is completed by applying unknownprop_50806ffdc0ac1326fa3eaa204e93d8bb855d8dd75aaaac9d3ef17ddfa41493cf.
The subproof is completed by applying unknownprop_d961c0e0be333ea5a20db7970c9827b32e18eeac074965e03b828f0add92cb19.
The subproof is completed by applying unknownprop_35207e33b98b51c17cc1fcfcaf6b2a30937bf1b76f7575cde92ec194f2bb140c.
The subproof is completed by applying unknownprop_1fb29a5203dbc910c36369870f9410f711bdcb9b217d23355b35e9355c51b8d5.
The subproof is completed by applying unknownprop_3c725ddec5fa6f7bfe8726974538e613fa221e94e96c7cb964bd6e1d400c0fe6.
The subproof is completed by applying unknownprop_270bc5f76005c0a11f71a1741219b544ee7a2c39bb0ac9fa4cec95721cbb71e6.
The subproof is completed by applying unknownprop_51d5ee2714328a86722ff59fa41d70943d26d8452c53b07ba6dbfe32c6c5b082.
The subproof is completed by applying unknownprop_035b42e1b8b8b6008931bc9da63c40c6ae1ec204fd511e4705e21961fbf64d00.