Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
Subq x0 x1,
Subq x1 x0,
ordinal (binunion x0 x1) leaving 3 subgoals.
Apply unknownprop_0f4c846b295f2eb5f79f47ff4ccb007f1db387ecfe4e8f437b57d42e2567ceb0 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_f4109d6144911b691369445da056f2ac2a55b5b3e1d67f32aee60b388a178b3a with
x0,
x1,
λ x2 x3 : ο . x3 ⟶ ordinal (binunion x0 x1).
Apply H2 with
λ x2 x3 . ordinal x3.
The subproof is completed by applying H1.
Apply unknownprop_f4109d6144911b691369445da056f2ac2a55b5b3e1d67f32aee60b388a178b3a with
x1,
x0,
λ x2 x3 : ο . x3 ⟶ ordinal (binunion x0 x1).
Apply unknownprop_6309f32475bcfc5c43876e0ea3ff21ee2bbf448bf4d934c2220eba39b2727bd5 with
x1,
x0,
λ x2 x3 . x3 = x0 ⟶ ordinal (binunion x0 x1).
Apply H2 with
λ x2 x3 . ordinal x3.
The subproof is completed by applying H0.