Apply and3I with
1bc5f.. = 1bc5f..,
64789.. 17d4e..,
64789.. 17d4e.. 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_8900aa9bfe05afa1f40e588aae88d401cf7435714fee66a8f40d56c6b91d7640.
The subproof is completed by applying unknownprop_8900aa9bfe05afa1f40e588aae88d401cf7435714fee66a8f40d56c6b91d7640.