Let x0 of type ι → (ι → ι → ι) → ι → ι be given.
Assume H0:
∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3.
Let x1 of type ι be given.
Apply unknownprop_9d8fc65a67d6e314245c05f0fc90054d64caf3cbb263534564051fb62d74e653 with
x0,
x1,
6445c.. x0 x1,
x0 x1 (6445c.. x0) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_6865caea2ddf8f4e2b7164a256811fa1fffb451c6311813215150a138627cda0 with
x0,
x1.
The subproof is completed by applying H0.
Apply unknownprop_1169691a14087b7b2b441ed75563e94dacee6760b95c7394fd506d4f6d512a0b with
x0,
x1.
The subproof is completed by applying H0.