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.
Apply H0 with
bij x1 x2 x4 ⟶ bij x0 x2 (λ x5 . x4 (x3 x5)).
Assume H1:
and (∀ x5 . prim1 x5 x0 ⟶ prim1 (x3 x5) x1) (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x3 x5 = x3 x6 ⟶ x5 = x6).
Assume H2:
∀ x5 . prim1 x5 x1 ⟶ ∃ x6 . and (prim1 x6 x0) (x3 x6 = x5).
Apply H1 with
bij x1 x2 x4 ⟶ bij x0 x2 (λ x5 . x4 (x3 x5)).
Assume H4:
∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x3 x5 = x3 x6 ⟶ x5 = x6.
Apply H5 with
bij x0 x2 (λ x5 . x4 (x3 x5)).
Assume H6:
and (∀ x5 . prim1 x5 x1 ⟶ prim1 (x4 x5) x2) (∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6).
Assume H7:
∀ x5 . prim1 x5 x2 ⟶ ∃ x6 . and (prim1 x6 x1) (x4 x6 = x5).
Apply H6 with
bij x0 x2 (λ x5 . x4 (x3 x5)).
Assume H9:
∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6.
Apply and3I with
∀ x5 . prim1 x5 x0 ⟶ prim1 (x4 (x3 x5)) x2,
∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x4 (x3 x5) = x4 (x3 x6) ⟶ x5 = x6,
∀ x5 . prim1 x5 x2 ⟶ ∃ x6 . and (prim1 x6 x0) (x4 (x3 x6) = x5) leaving 3 subgoals.
Let x5 of type ι be given.
Apply H8 with
x3 x5.
Apply H3 with
x5.
The subproof is completed by applying H10.
Let x5 of type ι be given.
Let x6 of type ι be given.
Assume H12: x4 (x3 x5) = x4 (x3 x6).
Apply H4 with
x5,
x6 leaving 3 subgoals.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
Apply H9 with
x3 x5,
x3 x6 leaving 3 subgoals.
Apply H3 with
x5.
The subproof is completed by applying H10.
Apply H3 with
x6.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
Let x5 of type ι be given.
Apply H7 with
x5,
∃ x6 . ... leaving 2 subgoals.