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