Apply unknownprop_b64a36774f7d36a62c02e6609cb70061f986c0fa39cbeaf25389ed0c08d877de with
8dd2c.. leaving 2 subgoals.
The subproof is completed by applying unknownprop_14a4ee8538d143fe8dc45eb2eb967d12f82b99130422357962aa2d0a55ab88f9.
The subproof is completed by applying unknownprop_57b8ec8100fb47d95fd7bcee1eb4fed21bcf07a9bbfc00cf18bdb9c88823060f.