Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_e546e9a8cc28c7314a8604ada98e2a83641f2ef6b8078441570ffe037b28d26f with
x0,
λ x3 . ∃ x4 . x3 = aae7a.. x1 x4,
22ca9..,
x2,
prim1 (aae7a.. x1 x2) x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H2:
∃ x4 . x3 = aae7a.. x1 x4.
Apply H2 with
prim1 (aae7a.. x1 x2) x0.
Let x4 of type ι be given.
Claim L5: x2 = x4
Apply H3 with
λ x5 x6 . x6 = x4.
Apply H4 with
λ x5 x6 . 22ca9.. x6 = x4.
The subproof is completed by applying unknownprop_916f469d850241375b1e44b2c6308f0113078869ceee129c02712fae69c32a37 with x1, x4.
Apply L5 with
λ x5 x6 . x3 = aae7a.. x1 x6.
The subproof is completed by applying H4.
Apply L6 with
λ x5 x6 . prim1 x5 x0.
The subproof is completed by applying H1.