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