| pf |
|---|
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply SNoLtLe_or with x1, x0, SNoLe x0 x1 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply FalseE with SNoLe x0 x1.
Apply SNoLtE with x1, x0, False leaving 6 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Apply SNoLt_irref with x1.
Apply SNoLt_tra with x1, x2, x1 leaving 5 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
The subproof is completed by applying H1.
The subproof is completed by applying H9.
Apply SNoLt_tra with x2, SNo_extend0 x0, x1 leaving 5 subgoals.
The subproof is completed by applying H5.
Apply SNo_extend0_SNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply binintersectE2 with SNoLev x1, SNoLev x0, SNoLev x2.
The subproof is completed by applying H6.
Apply SNoLtI2 with x2, SNo_extend0 x0 leaving 3 subgoals.
Apply SNo_extend0_SNoLev with x0, λ x3 x4 . SNoLev x2 ∈ x4 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply ordsuccI1 with SNoLev x0, SNoLev x2.
The subproof is completed by applying L13.
Apply SNoEq_tra_ with SNoLev x2, x2, x0, SNo_extend0 x0 leaving 2 subgoals.
The subproof is completed by applying H8.
Apply SNoEq_antimon_ with SNoLev x0, SNoLev x2, x0, SNo_extend0 x0 leaving 3 subgoals.
Apply SNoLev_ordinal with x0.
The subproof is completed by applying H0.
The subproof is completed by applying L13.
Apply SNoEq_sym_ with SNoLev x0, SNo_extend0 x0, x0.
Apply SNo_extend0_SNoEq with x0.
The subproof is completed by applying H0.
Apply SNoEq_E2 with SNoLev x0, SNo_extend0 x0, x0, SNoLev x2 leaving 3 subgoals.
Apply SNo_extend0_SNoEq with x0.
The subproof is completed by applying H0.
The subproof is completed by applying L13.
The subproof is completed by applying H12.
The subproof is completed by applying H3.
Apply SNoLt_irref with SNo_extend0 x0.
Apply SNoLt_tra with SNo_extend0 x0, x1, SNo_extend0 x0 leaving 5 subgoals.
Apply SNo_extend0_SNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply SNo_extend0_SNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Apply SNoLtI2 with x1, SNo_extend0 x0 leaving 3 subgoals.
Apply SNo_extend0_SNoLev with x0, λ x2 x3 . SNoLev x1 ∈ x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply ordsuccI1 with SNoLev x0, SNoLev x1.
The subproof is completed by applying H5.
Apply SNoEq_tra_ with SNoLev x1, x1, x0, SNo_extend0 x0 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply SNoEq_antimon_ with SNoLev x0, SNoLev x1, x0, SNo_extend0 x0 leaving 3 subgoals.
Apply SNoLev_ordinal with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
Apply SNoEq_sym_ with SNoLev x0, SNo_extend0 x0, x0.
Apply SNo_extend0_SNoEq with x0.
The subproof is completed by applying H0.
Apply SNoEq_E2 with SNoLev x0, SNo_extend0 x0, x0, SNoLev x1 leaving 3 subgoals.
Apply SNo_extend0_SNoEq with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
The subproof is completed by applying H7.
Apply FalseE with SNoEq_ (SNoLev x0) x1 x0 ⟶ nIn (SNoLev x0) x1 ⟶ False.
Apply ordsuccE with SNoLev x0, SNoLev x1, False leaving 3 subgoals.
The subproof is completed by applying H2.
Apply In_no2cycle with SNoLev x1, SNoLev x0 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H5.
Apply In_irref with SNoLev x1.
Apply H6 with λ x2 x3 . x3 ∈ SNoLev x1.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
■ |
|