The subproof is completed by applying unknownprop_e96dbc98c3bbaccd959c44021711d14fb0c42be8979571d40cfb87c8bcb73964 with 0.
Apply unknownprop_85c607d7f15e77a5ee8f24bb05830fb15170c21057f991be7770690abd21f820 with
Sing 0,
λ x0 x1 . 0,
λ x0 x1 . 0,
λ x0 x1 . 0,
Sing 0,
λ x0 x1 . 0,
λ x0 x1 x2 . 0,
λ x0 x1 . 0,
λ x0 x1 x2 . 0,
λ x0 x1 x2 . 0,
λ x0 x1 . 0,
λ x0 x1 . 0,
λ x0 x1 . 0,
λ x0 x1 . 0,
0,
0,
0,
0,
0 leaving 7 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L0.
The subproof is completed by applying L0.
The subproof is completed by applying L0.
The subproof is completed by applying L0.
The subproof is completed by applying unknownprop_a591d0e526a7dd2f8c99e9976c0392faf11d948523b13cba3a2ec28e3cc1875f.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
0 = Sing 0.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
0.
Apply H1 with
λ x0 x1 . In 0 x1.
The subproof is completed by applying unknownprop_e96dbc98c3bbaccd959c44021711d14fb0c42be8979571d40cfb87c8bcb73964 with 0.