Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply andI with
x0 = x2,
x1 = x3 leaving 2 subgoals.
Apply unknownprop_20aee288fe544593cb730f361570be2fc95d6b53d7a983cf10cd18dc24e2d96a with
x0,
x1,
x2,
x3 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
Apply unknownprop_1a9222940441343d3950b4eb89809bcf78424e1f44385bb97272c35b14b298d2 with
x0,
x1,
x2,
x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.