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 unknownprop_032ead5b4c5f033236ffe1882f61d2d26f3999d82c1400108a95074fe705e760 with
e6316.. x2 x1,
e6316.. x0 x3,
e6316.. x2 x3 leaving 3 subgoals.
Apply unknownprop_31bbde602545946a47b4dac3a1631f4d0f6a7c731ffc176f15f6d33d56c4598b with
x2,
x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Apply unknownprop_31bbde602545946a47b4dac3a1631f4d0f6a7c731ffc176f15f6d33d56c4598b with
x0,
x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Apply unknownprop_31bbde602545946a47b4dac3a1631f4d0f6a7c731ffc176f15f6d33d56c4598b with
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.