Apply unknownprop_836c46a9b0aab0b5cbed2984495126050b0c7cc3bccfb2fbb00fa0b927fb7a52 leaving 2 subgoals.
The subproof is completed by applying unknownprop_2f6bea85bf551d571e0bf7027d94b7d4069309ac241218bd56187772c492d512.
The subproof is completed by applying unknownprop_8044cc6a4d50a12b7b8e00ed59a3e6d96d53d14ea98fa842083fde4d42acddf6.