Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ο be given.
Assume H2: x0 = x1 ⟶ x2.
Assume H3:
∀ x3 . x3 ∈ SNoL x1 ⟶ x3 ∈ SNoR x0 ⟶ x2.
Assume H4:
x0 ∈ SNoL x1 ⟶ x2.
Assume H5:
x1 ∈ SNoR x0 ⟶ x2.
Assume H6:
∀ x3 . x3 ∈ SNoR x1 ⟶ x3 ∈ SNoL x0 ⟶ x2.
Assume H7:
x0 ∈ SNoR x1 ⟶ x2.
Assume H8:
x1 ∈ SNoL x0 ⟶ x2.
Apply SNoLt_trichotomy_or_impred with
x0,
x1,
x2 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply SNoLt_SNoL_or_SNoR_impred with
x0,
x1,
x2 leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H9.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Assume H9: x0 = x1.
Apply H2.
The subproof is completed by applying H9.
Apply SNoLt_SNoL_or_SNoR_impred with
x1,
x0,
x2 leaving 6 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H9.
Let x3 of type ι be given.
Assume H10:
x3 ∈ SNoL x0.
Assume H11:
x3 ∈ SNoR x1.
Apply H6 with
x3 leaving 2 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying H10.
The subproof is completed by applying H8.
The subproof is completed by applying H7.