Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_afad416180b684a18d95f2388cbc43118b2276df134d8618e716424654e613ec with
02a50.. x0 x1,
x0,
x1 leaving 3 subgoals.
Apply unknownprop_1d872d2fba72bbfb8f4867fe821cad13fefb27fee73f2ea0a29574094d71a01c with
x0,
x1.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H1.