Let x0 of type ι be given.
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with
b5c9f.. x0 x0,
λ x1 . bij x0 x0 (λ x2 . f482f.. x1 x2),
0fc90.. x0 (λ x1 . x1) leaving 2 subgoals.
Apply unknownprop_78f4273a7b4d13f02d77d194b65be481121674fd021f4ffb88d69be4bcd0ab71 with
x0,
λ x1 . x0,
λ x1 . x1.
Let x1 of type ι be given.
The subproof is completed by applying H0.
Apply and3I with
∀ x1 . prim1 x1 x0 ⟶ prim1 (f482f.. (0fc90.. x0 (λ x2 . x2)) x1) x0,
∀ x1 . prim1 x1 x0 ⟶ ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 (λ x3 . x3)) x1 = f482f.. (0fc90.. x0 (λ x3 . x3)) x2 ⟶ x1 = x2,
∀ x1 . prim1 x1 x0 ⟶ ∃ x2 . and (prim1 x2 x0) (f482f.. (0fc90.. x0 (λ x3 . x3)) x2 = x1) leaving 3 subgoals.
Let x1 of type ι be given.
Apply unknownprop_b456609235d152f08bccfce314d541d7c44f3716137c00b0ce21cf467ba83d17 with
x0,
λ x2 . x2,
x1,
λ x2 x3 . prim1 x3 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_b456609235d152f08bccfce314d541d7c44f3716137c00b0ce21cf467ba83d17 with
x0,
λ x3 . x3,
x1,
λ x3 x4 . x4 = f482f.. (0fc90.. x0 (λ x5 . x5)) x2 ⟶ x1 = x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_b456609235d152f08bccfce314d541d7c44f3716137c00b0ce21cf467ba83d17 with
x0,
λ x3 . x3,
x2,
λ x3 x4 . x1 = x4 ⟶ x1 = x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2: x1 = x2.
The subproof is completed by applying H2.
Let x1 of type ι be given.
Let x2 of type ο be given.
Apply H1 with
x1.
Apply andI with
prim1 x1 x0,
f482f.. (0fc90.. x0 (λ x3 . x3)) x1 = x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_b456609235d152f08bccfce314d541d7c44f3716137c00b0ce21cf467ba83d17 with
x0,
λ x3 . x3,
x1.
The subproof is completed by applying H0.