Let x0 of type ι → ο be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Apply unknownprop_385ff84ec085c257c4301120543ebbd86d07ea3e038f5ea5c342d81eb0c186da 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.