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_034efb78ebb5063d16d232d7a2af450524a44508ccd003479f3d4a1b105247b8 with
x0,
λ x2 . (∀ x3 . IrreflexiveSymmetricReln 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 ⟶ x3 x4 x5 ⟶ x3 x5 x4.
Apply H6 with
pack_r (prim4 x2) (λ x4 x5 . not (x4 = x5)),
False leaving 2 subgoals.
The subproof is completed by applying L7.