Let x0 of type ι be given.
Apply unknownprop_5273a64cd2d40c560fbf5871c7601206337acc93fe8f7292cc8c65a171682421 with
λ x1 x2 : ι → ο . x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ x2 x3.
Let x1 of type ι be given.
Apply andE with
TransSet x0,
∀ x2 . In x2 x0 ⟶ TransSet x2,
and (TransSet x1) (∀ x2 . In x2 x1 ⟶ TransSet x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
TransSet x1,
∀ x2 . In x2 x1 ⟶ TransSet x2 leaving 2 subgoals.
Apply H3 with
x1.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x1,
x0,
x2 leaving 2 subgoals.
Apply unknownprop_694898c9791aec4140fc01c2b4287388fd1297142d7e1ee2585d4a7ba4f43dce with
λ x3 x4 : ι → ο . x3 x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
Apply H3 with
x2.
The subproof is completed by applying L5.