Apply unknownprop_a90cef7a0ba9512cc0d2e629e580894b6ddc586580e86ce1ae226da918648109 with
Sing 1,
1,
0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_e96dbc98c3bbaccd959c44021711d14fb0c42be8979571d40cfb87c8bcb73964 with 1.
The subproof is completed by applying unknownprop_b28daf094ddd549776d741eec1dac894d28f0f162bae7bdbdbfb7366b31cdef0.