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: d8424.. x3 x1.
Apply H5 with 5bab1.. x0 x1 leaving 12 subgoals.
Apply unknownprop_6a5c8c3c4e98ceac19f21d91065cc17f225fc39d17a06fb013c2917c0979a01e 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_7f008da2dfa9feb835387c0f0cbb3f8553b3774515c7d81e349bbd1bce5b9bf7 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_64e2c5cc8574a7172ca961c3e547317c067131392674e1c7450d6cf4c17c80da 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_f59b25790e83b462660170da7f0a0926fc3308098a12059c6fb644ad271db8ab 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_5955780e2b0d6b64c3b7f3187ffc8740ad8ea8e0d039060e0416e8070c73b28a 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_92be4aa1e2d120c79d61d6dfc974e310772f7dec2ea22f92bf78e127cca2414b 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_3cf1b4d63ffa97c570a31d3fc1201ac8228ce55e97b64b5e07d910608ca7c24d 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_5663fe7922f65c5d33bb45030018c36c5cbcb4a20b316bd4f71014a9ae88caf3 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_237bd744af43bc2714eb329c2fb349aa061083e5646cc924d9a147c6ba9fb4ab 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_596a3ea4959170e717984662f74cd601a84212bf8ec6e83b934b9b78ed875c50 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_885c508bb242b50d81d3c1f56c4d48d6e46d8b868d3ce8a40020cf4478fe65d8 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_a9e52ae1e08eb19e7f8886398a460124b2a1acef86066fd39f7c2390f5ea7a7c 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.
■