| 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.
Let x2 of type ι be given.
Assume H3: x2 ∈ x0.
Let x3 of type ι be given.
Apply H5 with 5bab1.. x0 x1 leaving 14 subgoals.
Apply unknownprop_091ea6faa0f9a3a2fade06dcb43725a6b4000e38553062a0c29186dc40023182 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_f18a142872a9f8cd414d95bb96fe461622fd2664d7fc6662f9f9f830a3aa5f33 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_406783b38766f62def6edb5e8e684675a02f99d0126414d36b30d1e06dbeddc9 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_ec613f9d199c12bbb0070ce78ae42dfc3053e1abd31a53fe1f2bbf25194b9fe3 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_b0fbad19560a20ccd0b0ba1b5c77e22502047170c7f1c8b5f850fd602b0fb0a5 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_26d552676ea6379024dd96979ce0463cd095c83ce13277d84dbd704acffeb699 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_68ba9acdde2ed33f1191454e74f8ed6ebb3c56fc9a0b6aee82622110fd7f5a44 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_48788008fb0c645d201637984f1a508e33b3336b26673f83e069805e91e46124 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_440e6657211cc602621eb532b02c4c910e1794c19624695e6cf816daf09e5052 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_8105d51ee69c98fcd2ab31bba30658564593ceb8a7fb6d5850b6911d9f28cddc 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_0a34240f5319ca4396d7dd8668b386bacb97ecb490ccf4447c3235292c027927 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_2115435579b634d60f6aa508bf153bede97caef90419ea7ca9f34226c8ba0114 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_560f66d9d4c3decaf7cc78ddc5f1e3146d1ce7fc52c8dd8bab8105f2e242e107 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_1239c169c89698822dc8d3085a3891580645c3385a5592d758e9edee6c02cc84 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.
■ |
|