Let x0 of type ι → ι → ο be given.
Assume H0: ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1.
Assume H1:
∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3).
Assume H2:
∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3)).
Let x1 of type ι be given.
Apply unknownprop_e218ed8cf74f73d11b13279ecb43db2e902573ebd411cc1f7c1f71620f4a5da3 with
setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1)),
u12 leaving 2 subgoals.
Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with
u12,
setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1)),
atleastp (setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))) u12 leaving 3 subgoals.
The subproof is completed by applying nat_12.
The subproof is completed by applying H5.
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with
u18,
atleastp (setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))) u12 leaving 2 subgoals.
The subproof is completed by applying unknownprop_b6349b103ec0c23863292fe6c57a85341c64566cbff4099647a6f20c72c67730.
Apply atleastp_tra with
u19,
setsum u13 u6,
u18 leaving 2 subgoals.
Apply equip_atleastp with
u19,
setsum u13 u6.
Apply unknownprop_e5120d40f4a32c7af3d0d388c476457842e1606aa91e4ca1062133e04a054af7 with
λ x2 x3 . equip x2 (setsum u13 u6).
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with
u13,
u6,
u13,
u6 leaving 4 subgoals.
The subproof is completed by applying nat_13.
The subproof is completed by applying nat_6.
The subproof is completed by applying equip_ref with
u13.
The subproof is completed by applying equip_ref with
u6.