Let x0 of type ι be given.
Apply unknownprop_5273a64cd2d40c560fbf5871c7601206337acc93fe8f7292cc8c65a171682421 with
λ x1 x2 : ι → ο . TransSet x0 ⟶ (∀ x3 . In x3 x0 ⟶ TransSet x3) ⟶ x2 x0.
The subproof is completed by applying unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
TransSet x0,
∀ x1 . In x1 x0 ⟶ TransSet x1.