Apply unknownprop_69127496054dee8936aec576c0d8ea811a7839ce114f58c0a3de34ea0d529229 with
8dd2c..,
c6963.. leaving 3 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.