Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Assume H2:
∀ x3 . prim1 x3 x0 ⟶ x2 x3 = x1 ⟶ ∀ x4 : ο . x4.
Assume H3:
∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.
Assume H4:
∀ x3 : ι → ο . x3 x1 ⟶ (∀ x4 . x3 x4 ⟶ x3 (x2 x4)) ⟶ ∀ x4 . prim1 x4 x0 ⟶ x3 x4.
Apply and5I with
prim1 x1 x0,
∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x0,
∀ x3 . prim1 x3 x0 ⟶ x2 x3 = x1 ⟶ ∀ x4 : ο . x4,
∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4,
∀ x3 : ι → ο . x3 x1 ⟶ (∀ x4 . x3 x4 ⟶ x3 (x2 x4)) ⟶ ∀ x4 . prim1 x4 x0 ⟶ x3 x4 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.