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