Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Apply unknownprop_889c17b99dca376b4b055d4894926d0ecc6abc4200cea43a8b3c95ddc508b1ab with
λ x2 x3 : ι → (ι → ι → ι) → ι → ι . x3 x0 x1 0 = x0.
Apply unknownprop_b46ce29ff1d7f9d2e6d60e6a0f6f0736a07c8ba94a4f18feca3e51921a7ff153 with
λ x2 . λ x3 : ι → ι . If_i (In (Union x2) x2) (x1 (Union x2) (x3 (Union x2))) x0,
0,
λ x2 x3 . x3 = x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_e652f066d9435ede645bc10d8cd2fb7bcf5eb83fa0002bee8f12740ed64e8fbe with x0, x1.
Apply unknownprop_5a150bd86f4285de5d98c60b17d4452a655b4d88de0a02247259cdad6e6d992c with
In (Union 0) 0,
x1 (Union 0) (In_rec_poly_i (λ x2 . λ x3 : ι → ι . If_i (In (Union x2) x2) (x1 (Union x2) (x3 (Union x2))) x0) (Union 0)),
x0.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
In (Union 0) 0.
The subproof is completed by applying unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
Union 0.