The subproof is completed by applying unknownprop_e96dbc98c3bbaccd959c44021711d14fb0c42be8979571d40cfb87c8bcb73964 with 0.
Apply unknownprop_cea6fa3bef113861342fee1a89745a02fcf39fdc2d393afb77330bbc238e9f5e 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 leaving 6 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 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.