Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
In x0 (V_ x1),
Subq (V_ x1) (V_ x0),
or (In (V_ x0) (V_ x1)) (Subq (V_ x1) (V_ x0)) leaving 3 subgoals.
The subproof is completed by applying unknownprop_237254741ee4851b76b4cc2153c4d1b06fbb6553611a04bed6f42e10664ad562 with x0, x1.
Assume H0:
In x0 (V_ x1).
Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with
In (V_ x0) (V_ x1),
Subq (V_ x1) (V_ x0).
Apply unknownprop_1ddbc38515addbc9ee4e65ef2c7bb2a459b929b93d42b919e6742e2022098301 with
x0,
x1.
The subproof is completed by applying H0.
Apply unknownprop_c29620ea10188dd8ed7659bc2875dc8e08f16ffd29713f8ee3146f02f9828ceb with
In (V_ x0) (V_ x1),
Subq (V_ x1) (V_ x0).
The subproof is completed by applying H0.