Apply unknownprop_5273a64cd2d40c560fbf5871c7601206337acc93fe8f7292cc8c65a171682421 with
λ x0 x1 : ι → ο . x1 0.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
TransSet 0,
∀ x0 . In x0 0 ⟶ TransSet x0 leaving 2 subgoals.
Apply unknownprop_694898c9791aec4140fc01c2b4287388fd1297142d7e1ee2585d4a7ba4f43dce with
λ x0 x1 : ι → ο . x1 0.
Let x0 of type ι be given.
Apply FalseE with
Subq x0 0.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
x0.
The subproof is completed by applying H0.
Let x0 of type ι be given.
Apply FalseE with
TransSet x0.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
x0.
The subproof is completed by applying H0.