Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Claim L1:
∃ x3 . and (In x3 x0) (x1 x2 = x1 x3)Apply unknownprop_c98758e554c059e2dd4a74de2bd87519acf2bfbb61d2d69b0a8aac8c25bb1b4c with
λ x3 . In x3 x0,
λ x3 . x1 x2 = x1 x3,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι → ι → ο be given.
Assume H1: x3 (x1 x2) (x1 x2).
The subproof is completed by applying H1.
Apply unknownprop_d5d9d085d36b1ca4854d01b78e983bcd20b298e2776d1ae6d4a1dc3393a026ac with
In (x1 x2) (Repl x0 (λ x3 . x1 x3)),
∃ x3 . and (In x3 x0) (x1 x2 = x1 x3) leaving 2 subgoals.
The subproof is completed by applying unknownprop_422bc2d8d5c5891fd637c087651fa7529b2c1da4bb1da1788f9bfacb9979ef9e with x0, x1, x1 x2.
The subproof is completed by applying L1.