Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_909c4bbc49234990ae4796a77dae45da4e74d98f1a4117290a493db105a3b619 with
x0,
x1,
∀ x2 : ο . (∀ x3 . SNo x3 ⟶ In (SNoLev x3) (binintersect (SNoLev x0) (SNoLev x1)) ⟶ SNoEq_ (SNoLev x3) x3 x0 ⟶ SNoEq_ (SNoLev x3) x3 x1 ⟶ SNoLt x0 x3 ⟶ SNoLt x3 x1 ⟶ nIn (SNoLev x3) x0 ⟶ In (SNoLev x3) x1 ⟶ x2) ⟶ (In (SNoLev x0) (SNoLev x1) ⟶ SNoEq_ (SNoLev x0) x0 x1 ⟶ In (SNoLev x0) x1 ⟶ x2) ⟶ (In (SNoLev x1) (SNoLev x0) ⟶ SNoEq_ (SNoLev x1) x0 x1 ⟶ nIn (SNoLev x1) x0 ⟶ x2) ⟶ x2.
Let x2 of type ο be given.
Apply unknownprop_7d798c5794ed96c61cc9ec828963a5831eee43021e8f1ea48be05a5cb53904e0 with
SNoLev x0,
SNoLev x1,
λ x3 . In x3 x0,
λ x3 . In x3 x1,
x2 leaving 4 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_ff2db5d7cd089ead6d3f23ab1904a643f023d611ddbe42c5c85e87e080e26158 with
binintersect (SNoLev x0) (SNoLev x1),
λ x3 . In x3 x0,
λ x3 . In x3 x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H8.
Let x3 of type ι be given.
Assume H10:
PNoEq_ x3 (λ x4 . In x4 x0) (λ x4 . In x4 x1).
Assume H11:
not (In x3 x0).
Apply unknownprop_9f9c1680d203bdbb862d1bf6c2b8504d7e3a6fca72f77bd8968e86ad6ad69346 with
SNoLev x0,
SNoLev x1,
x3,
x2 leaving 2 subgoals.
The subproof is completed by applying H9.
Apply unknownprop_97c7da29e9595b010ed33a7cba4535d53c32ea3bcafdf9fb46c420ab4230017e with
PSNo x3 (λ x4 . In x4 x0),
x2 leaving 2 subgoals.
The subproof is completed by applying L17.