Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_5a150bd86f4285de5d98c60b17d4452a655b4d88de0a02247259cdad6e6d992c with
In 0 0,
x0,
x1,
λ x2 x3 . In x2 (UPair x0 x1) leaving 2 subgoals.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
In 0 0.
The subproof is completed by applying unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with 0.
Apply unknownprop_cbe03b1d73461065a9cab3cfe58a3146c30e691f6f669990a6f43a4ec94a2bbe with
λ x2 x3 : ι → ι → ι . In (If_i (In 0 0) x0 x1) (x3 x0 x1).
Apply unknownprop_63c308b92260dbfca8c9530846e6836ba3e6be221cc8e80fd61db913e01bdacf with
Power (Power 0),
λ x2 . If_i (In 0 x2) x0 x1,
0.
The subproof is completed by applying unknownprop_8285cfa4fcfced8bf8f28f246aaeb081e0d4a211d67c239e326650337a8e69c8 with
Power 0.