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 8 subgoals.
Apply unknownprop_980ded8cbfc1b90a4fe56940f1963d452ec52fb2102e5e1b85b8e4c30764bc41 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_74d69e5cfedfad33160bd6f66288614a41abbef991042edcc2f22bd8692d2ad9 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_8806714be516252c5ebc78070b2b236c3a9ba8045c653af85bdf99cba29e0544 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_a4faad2bc838cc7f29f2b73a017b51405895bba23aa738f96583faa4a837d4c5 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_fb59b6acfbb34d9190841699bda961275bd746eaf19fda0babae65fe2d24fae8 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_b05830c71e1f162207cd6b318d1795660e83efd7c5b47b448a2c87eac97d4045 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_85110c3ad5b253b1838ac4eecc91753f016d7532ac1dae9bab77d29703f8149a 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_82b892ad037827628f79739044ea40b9cef6912e36888f955071d5e2c53bb12f 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.