Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι → ι → ι be given.
Let x4 of type ι → ι → ι be given.
Let x5 of type ι → ι → ο be given.
Let x6 of type ι → ι → ι be given.
Assume H0:
62ee1.. x0 x1 x2 x3 x4 x5.
Assume H1:
∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ x6 x7 x8 = x6 x9 x10 ⟶ and (x7 = x9) (x8 = x10).
Apply unknownprop_e360b425f900a376ca06fcd10fba4a915b77c9a8984949bc73d964f2c814f078 with
x0,
x1,
x2,
x3,
x4,
x5,
x6 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_24a53e117993637ef093c07d5478d6eab76227309103f5a358a7a9915d16e9e1 with
x0,
x1,
x2,
x3,
x4,
x5,
x6 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_0895ab7e77032697f87c3e2018c1e511e65b450716c5d718faef2a58fd68ca7e with
x0,
x1,
x2,
x3,
x4,
x5,
x6 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_7987aafa18a38f2416ba6bf9c67b127bb897db4d79b296328a85371faabbd242 with
x0,
x1,
x2,
x3,
x4,
x5,
x6 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.