Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0:
In x0 (V_ x1).
Apply unknownprop_3687558d9284fdd514174bfe87bba39032212334a6409eb4554d4077dea6d831 with
x0,
x1,
In (V_ x0) (V_ x1) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply unknownprop_a2c3fca2e8c461af2fcd2014916bc97ec486da998a233beedf90ec14d6bf2e76 with
V_ x0,
x2,
x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_9143b3674c790ed26c1d41216fe3742a8002230ba5cffca45c4cf28cb75c4718 with
x0,
x2.
The subproof is completed by applying H2.