Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Let x2 of type ι → ι be given.
Let x3 of type ι be given.
Apply unknownprop_04b90adbc2ec31bffcbccbbe8e8bda04aa9f95ec157434af0f1f260c2db4f24e with
1216a.. x0 (λ x4 . x1 x4),
x2,
x3,
∃ x4 . and (prim1 x4 x0) (and (x1 x4) (x3 = x2 x4)) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x4 of type ι be given.
Apply H1 with
∃ x5 . and (prim1 x5 x0) (and (x1 x5) (x3 = x2 x5)).
Assume H3: x3 = x2 x4.
Apply unknownprop_e4362c04e65a765de9cf61045b78be0adc0f9e51a17754420e1088df0891ff67 with
x0,
x1,
x4,
∃ x5 . and (prim1 x5 x0) (and (x1 x5) (x3 = x2 x5)) leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H5: x1 x4.
Let x5 of type ο be given.
Assume H6:
∀ x6 . and (prim1 x6 x0) (and (x1 x6) (x3 = x2 x6)) ⟶ x5.
Apply H6 with
x4.
Apply andI with
prim1 x4 x0,
and (x1 x4) (x3 = x2 x4) leaving 2 subgoals.
The subproof is completed by applying H4.
Apply andI with
x1 x4,
x3 = x2 x4 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H3.