Apply unknownprop_1c4b77a1bdf71ac8c46772d8b01bd6609e54ee74070e16498c4800adfe13c5ca with
0,
0,
1,
0 leaving 4 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNo_0.