Let x0 of type ι be given.
Apply unknownprop_5273a64cd2d40c560fbf5871c7601206337acc93fe8f7292cc8c65a171682421 with
λ x1 x2 : ι → ο . x2 x0.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
TransSet x0,
∀ x1 . In x1 x0 ⟶ TransSet x1 leaving 2 subgoals.
Apply unknownprop_691e57c539f219e8b63c6900720d2387f320621de398fcaf8bd5551ad6c0dc08 with
x0.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Apply unknownprop_691e57c539f219e8b63c6900720d2387f320621de398fcaf8bd5551ad6c0dc08 with
x1.
Apply unknownprop_3069c6fa8dbd033f1c94555c93d580ac5c2fd979807cb20dbdb8dc4cc9b1517f with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.