Let x0 of type ι → ο be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Apply unknownprop_75289f459b64a3ccf905872abdf8e8faec9a64bfbf4b807de994618fe828d97a with
x0,
57d6a.. (56103.. x1) x2,
x1 x2.
Apply unknownprop_926cc02c4f098fe564160a6c61812d6c198ad701faef425ec2ce9a51e9a7b7e0 with
x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.