Apply H0 with
False.
Let x0 of type ι be given.
Apply H1 with
False.
Let x1 of type ι → ι be given.
Apply H2 with
False.
Apply unknownprop_2d7c7a9916fa2967cfb4d546f4e37c43b64368ed4a60618379328e066e9b7e0e with
x0,
λ x2 . (∀ x3 . IrreflexiveTransitiveReln x3 ⟶ and (BinRelnHom x3 x2 (x1 x3)) (∀ x4 . BinRelnHom x3 x2 x4 ⟶ x4 = x1 x3)) ⟶ False leaving 2 subgoals.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Let x3 of type ι → ι → ο be given.
Assume H4:
∀ x4 . x4 ∈ x2 ⟶ not (x3 x4 x4).
Assume H5: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ x3 x4 x5 ⟶ x3 x5 x6 ⟶ x3 x4 x6.