Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_5c4c172738689d5a3fd02bb243809a41a7c0e7ed334ee0cdfb9155b4865de4da with
SNoLev x0,
x0,
x1,
x0 = x1.
Apply unknownprop_738757eec61e36a7ed8ed03b81edd6c58e5dafd21ee5d9ae0df86b9a28226a9f with
SNoLev x0,
λ x2 . In x2 x0,
λ x2 . In x2 x1,
x0 = x1.
Assume H3:
∀ x2 . In x2 (SNoLev x0) ⟶ iff ((λ x3 . In x3 x0) x2) ((λ x3 . In x3 x1) x2).
Apply unknownprop_a23ec6a55ac212526d74cbf0d04096929ad453b0eb0f8023e32b8a33930d39fb with
x0,
x1 leaving 2 subgoals.
Apply unknownprop_3efe32fa3ae894b4dee8f8801443a9f632872bc10d5ad6c3b9f673ffccfc8b24 with
x0,
x1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply H2 with
λ x2 x3 . Subq (SNoLev x0) x2.
The subproof is completed by applying unknownprop_d889823a5c975ad2d68f484964233a1e69e7d67f0888aa5b83d962eeca107acd with
SNoLev x0.
The subproof is completed by applying H3.
Apply unknownprop_3efe32fa3ae894b4dee8f8801443a9f632872bc10d5ad6c3b9f673ffccfc8b24 with
x1,
x0 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply H2 with
λ x2 x3 . Subq (SNoLev x1) x3.
The subproof is completed by applying unknownprop_d889823a5c975ad2d68f484964233a1e69e7d67f0888aa5b83d962eeca107acd with
SNoLev x1.
Let x2 of type ι be given.
Apply unknownprop_dd64fd93d8daab6216880664465dfc3db916267bc5f0c0940bb7191cc10a2c43 with
In x2 x0,
In x2 x1.
Apply H3 with
x2.
Apply H2 with
λ x3 x4 . In x2 x4.
The subproof is completed by applying H4.