Let x0 of type ι be given.
Apply H0 with
struct_r x0.
Assume H2:
unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (∀ x3 . x3 ∈ x1 ⟶ not (x2 x3 x3)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3)).
The subproof is completed by applying H1.
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_034efb78ebb5063d16d232d7a2af450524a44508ccd003479f3d4a1b105247b8 with
x0,
λ x4 . IrreflexiveSymmetricReln (05907.. x4 x1 x2 x3) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x4 of type ι be given.
Let x5 of type ι → ι → ο be given.
Assume H5:
∀ x6 . x6 ∈ x4 ⟶ not (x5 x6 x6).
Assume H6: ∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ x5 x6 x7 ⟶ x5 x7 x6.
Apply unknownprop_f1f0d0235cc3f72918ba3b7bc6e671feb556f667a17378616f96007dc95611ad with
x4,
x5,
x1,
x2,
x3,
λ x6 x7 . IrreflexiveSymmetricReln x7.
Apply unknownprop_d442b731cc8a623579f119dd4140f334acbb8f35c49c35a487654154f8239ef6 with
{x6 ∈ x4|ap x2 x6 = ap x3 x6},
x5 leaving 2 subgoals.
Let x6 of type ι be given.
Assume H7:
x6 ∈ {x7 ∈ x4|ap x2 x7 = ap x3 x7}.
Apply H5 with
x6.
Apply SepE1 with
x4,
λ x7 . ap x2 x7 = ap x3 x7,
x6.
The subproof is completed by applying H7.
Let x6 of type ι be given.
Assume H7:
x6 ∈ {x7 ∈ x4|ap x2 x7 = ap x3 x7}.
Let x7 of type ι be given.
Assume H8:
x7 ∈ {x8 ∈ x4|ap x2 x8 = ap x3 x8}.
Assume H9: x5 x6 x7.
Apply H6 with
x6,
x7 leaving 3 subgoals.
Apply SepE1 with
x4,
λ x8 . ap x2 x8 = ap x3 x8,
x6.
The subproof is completed by applying H7.
Apply SepE1 with
x4,
λ x8 . ap x2 x8 = ap x3 x8,
x7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
Apply unknownprop_2aabccf4699c9f902dcc37be8ad1f3aaa001e5f2bb081556c38a4bbd69d3e5c6 with
IrreflexiveSymmetricReln leaving 2 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.