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