Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_6d861aa069d3c6b52ea4a1626e236a28ccef38ff01ec7a48d612e144c66b13b6 with
λ x3 x4 : ι → ι → ο . x4 x0 x1 ⟶ x4 x1 x2 ⟶ x4 x0 x2.
Let x3 of type ι → ι → ο be given.
Apply unknownprop_5574bdb5e5df6f14031f4de95b01de091bd6680b3f0f837fce12fa18146d5760 with
x3,
x3 x0 x2 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_4b6e1be37f965f13c2d93c65e0492a396bc7c89d8084e2ab41de476f9c36145c with
x3,
x0,
x1,
x2 leaving 3 subgoals.
The subproof is completed by applying H8.
Apply H0 with
x3 leaving 5 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Apply H1 with
x3 leaving 5 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H6.