Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι be given.
Assume H0:
∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3.
Let x3 of type ι be given.
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with
x0,
x1,
x3,
prim1 x3 (94f9e.. x0 x2) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x4 of type ι be given.
Assume H3: x3 = x1 x4.
Apply H3 with
λ x5 x6 . prim1 x6 (94f9e.. x0 (λ x7 . x2 x7)).
Apply H0 with
x4,
λ x5 x6 . prim1 x6 (94f9e.. x0 (λ x7 . x2 x7)) leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with
x0,
x2,
x4.
The subproof is completed by applying H2.