Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Let x2 of type ι be given.
Apply unknownprop_889c17b99dca376b4b055d4894926d0ecc6abc4200cea43a8b3c95ddc508b1ab with
λ x3 x4 : ι → (ι → ι → ι) → ι → ι . x4 x0 x1 (ordsucc x2) = x1 x2 (x4 x0 x1 x2).
Apply unknownprop_b46ce29ff1d7f9d2e6d60e6a0f6f0736a07c8ba94a4f18feca3e51921a7ff153 with
λ x3 . λ x4 : ι → ι . If_i (In (Union x3) x3) (x1 (Union x3) (x4 (Union x3))) x0,
ordsucc x2,
λ x3 x4 . x4 = x1 x2 (In_rec_poly_i (λ x5 . λ x6 : ι → ι . If_i (In (Union x5) x5) (x1 (Union x5) (x6 (Union x5))) x0) x2) leaving 2 subgoals.
The subproof is completed by applying unknownprop_e652f066d9435ede645bc10d8cd2fb7bcf5eb83fa0002bee8f12740ed64e8fbe with x0, x1.
Apply unknownprop_10a14ccca528cf09b2b630c2b3ad6b12861bd3388858019b163d7ab740a6a5c8 with
x2,
λ x3 x4 . If_i (In x4 (ordsucc x2)) (x1 x4 (In_rec_poly_i (λ x5 . λ x6 : ι → ι . If_i (In (Union x5) x5) (x1 (Union x5) (x6 (Union x5))) x0) x4)) x0 = x1 x2 (In_rec_poly_i (λ x5 . λ x6 : ι → ι . If_i (In (Union x5) x5) (x1 (Union x5) (x6 (Union x5))) x0) x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_6f44febdf8a865ee94133af873e3c2941a931de6ac80968301360290e02ca608 with
In x2 (ordsucc x2),
x1 x2 (In_rec_poly_i (λ x3 . λ x4 : ι → ι . If_i (In (Union x3) x3) (x1 (Union x3) (x4 (Union x3))) x0) x2),
x0.
The subproof is completed by applying unknownprop_4b3850b342b3607d712ced4e4c9fa37dbdc70692760e3dc82f8fd86e9b26a6b5 with x2.