Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
Power 0,
Sing 0 leaving 2 subgoals.
Let x0 of type ι be given.
Claim L1: x0 = 0
Apply unknownprop_73b312e5c0ced1987581817c61d2a6ab9e4c47a87f99557a6b2723117244e7d9 with
x0.
Apply unknownprop_b8811722bb772bba243207d8ee471ba24f8b88e821f7737307414168e638d2c6 with
0,
x0.
The subproof is completed by applying H0.
Apply L1 with
λ x1 x2 . In x2 (Sing 0).
The subproof is completed by applying unknownprop_e96dbc98c3bbaccd959c44021711d14fb0c42be8979571d40cfb87c8bcb73964 with 0.
Let x0 of type ι be given.
Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with
0,
x0,
λ x1 x2 . In x2 (Power 0) leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_8285cfa4fcfced8bf8f28f246aaeb081e0d4a211d67c239e326650337a8e69c8 with 0.