Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_4358b1b5e793b47fce3fac2d82616bfe2f6625cb01f2397277ef761d656463ce with
x2,
λ x3 x4 . In x0 x4.
Apply unknownprop_4d9a081a15fdc79c67eee9fe67650a775bc97737c16f9cc2a1a6fdd7a2cc8108 with
x2,
λ x3 . Power (V_ x3),
x1,
x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_9a40b4678ae1931e61346f9ab9e405ec760f2f9d44b3be548b52a8b2ddb78559 with
V_ x1,
x0.
The subproof is completed by applying H1.