Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Assume H0: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2.
Assume H1: 4402e.. x0 x1.
Assume H2: cf2df.. x0 x1.
Let x2 of type ι be given.
Assume H3: x2 ∈ x0.
Let x3 of type ι be given.
Assume H4: x3 ⊆ setminus x0 (Sing x2).
Assume H5: 71717.. x3 x1.
Apply H5 with 5bab1.. x0 x1 leaving 12 subgoals.
Apply unknownprop_b9c353fd56ffb9c0eca37d1f521c30deae88a5c801fceae415557c0e442cf153 with x0, x1, x2, x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply unknownprop_55ad6ace9724379c47f4dcc4298a88ee53c72620ba6ccd2dac8dcd98fbf1e1f0 with x0, x1, x2, x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply unknownprop_1dea0f26d4ccc022a69cf87304dd5299643b27578baf0ed880e9bdb57c72db66 with x0, x1, x2, x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply unknownprop_3ba81c9deb1af7096eb48cfce194f117c05ef936294f039575e8b517e10a40a4 with x0, x1, x2, x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply unknownprop_466d8041083bbc7b2af6e9d3edd5c6e542333a88e4363943aeb50a521a452cf0 with x0, x1, x2, x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply unknownprop_117d2367060244c89f0002b6a7b8345f3f0f11295c8718e2e8a7f3aa15bcd41a with x0, x1, x2, x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply unknownprop_fd7691248372d114e2c84ac9745635729ff6a3d4b55d92d52e0da90ed38d6caf with x0, x1, x2, x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply unknownprop_1fd75b83df0e035da10e6e91dc9b61b62fc7f9fdb1dc4d5a159636246d2960ba with x0, x1, x2, x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply unknownprop_b812c7d271ebd8bf88363d393d4bb473013ebdb507e97756c55c2014dc4c31d7 with x0, x1, x2, x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply unknownprop_72d1a91739d7fcca2cf3562bd44b5ab0df0e3114f68e226430195ecdb1cacfed with x0, x1, x2, x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply unknownprop_efeb18df5ce4cfa83b7401407ee6d05c13a35629921a69056147a10668b3486b with x0, x1, x2, x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply unknownprop_50af65bb21a3c1499ec027c97994da95b4405e6e5334cba32c97a9faa0439699 with x0, x1, x2, x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
■