Apply and3I with
cca5e.. = cca5e..,
64789.. 79919..,
64789.. 79919.. leaving 3 subgoals.
Let x0 of type (CT2 (CT2 (ι → ι → ι))) → (CT2 (CT2 (ι → ι → ι))) → ο be given.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_4237e1db3b44c4a64571a1c1c32c1feb5b80ca5727ff1508690c3893d070c688.
The subproof is completed by applying unknownprop_4237e1db3b44c4a64571a1c1c32c1feb5b80ca5727ff1508690c3893d070c688.