Apply unknownprop_1c4b77a1bdf71ac8c46772d8b01bd6609e54ee74070e16498c4800adfe13c5ca with
0,
0,
0,
1 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_0.
The subproof is completed by applying SNo_1.